diff options
Diffstat (limited to '')
-rw-r--r-- | src/Interpreter.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 2c4d86d2..a9a44b0f 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2,6 +2,7 @@ module L = Logging module T = Types module A = CfimAst module M = Modules +module SA = SymbolicAst open Cps open InterpreterUtils open InterpreterStatements @@ -170,8 +171,8 @@ module Test = struct List.iter test_unit_fun unit_funs (** Execute the symbolic interpreter on a function. *) - let test_function_symbolic (config : C.partial_config) (m : M.cfim_module) - (fid : A.FunDefId.id) : unit = + let test_function_symbolic (config : C.partial_config) (synthesize : bool) + (m : M.cfim_module) (fid : A.FunDefId.id) : unit = (* Retrieve the function declaration *) let fdef = A.FunDefId.nth m.functions fid in @@ -185,10 +186,11 @@ module Test = struct (* Create the continuation to check the function's result *) let cf_check res _ = match res with - | Return | Panic -> + | Return -> if synthesize then raise Errors.Unimplemented else None + | Panic -> (* Note that as we explore all the execution branches, one of * the executions can lead to a panic *) - None + if synthesize then Some SA.Panic else None | _ -> failwith ("Unit test failed (symbolic execution) on: " @@ -205,8 +207,8 @@ module Test = struct TODO: for now we ignore the functions which contain loops, because they are not supported by the symbolic interpreter. *) - let test_functions_symbolic (config : C.partial_config) (m : M.cfim_module) : - unit = + let test_functions_symbolic (config : C.partial_config) (synthesize : bool) + (m : M.cfim_module) : unit = let no_loop_funs = List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) m.functions in @@ -214,7 +216,7 @@ module Test = struct (* Execute the function - note that as the symbolic interpreter explores * all the path, some executions are expected to "panic": we thus don't * check the return value *) - test_function_symbolic config m def.A.def_id + test_function_symbolic config synthesize m def.A.def_id in List.iter test_fun no_loop_funs end |