diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Driver.ml | 5 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 30 |
2 files changed, 0 insertions, 35 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 476907c1..12a6f075 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -219,11 +219,6 @@ let () = (* Test the unit functions with the concrete interpreter *) if !test_unit_functions then I.Test.test_unit_functions m; - (* Evaluate the symbolic interpreter on the functions, ignoring the - * functions which contain loops - TODO: remove *) - let synthesize = true in - I.Test.test_functions_symbolic synthesize m; - (* Translate the functions *) Translate.translate_crate filename dest_dir m; diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index a69b7b51..ccb9009e 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -549,34 +549,4 @@ module Test = struct in () - - (** Small helper *) - let fun_decl_is_transparent (def : A.fun_decl) : bool = - Option.is_some def.body - - (** Execute the symbolic interpreter on a list of functions. - - TODO: for now we ignore the functions which contain loops, because - they are not supported by the symbolic interpreter. - *) - let test_functions_symbolic (synthesize : bool) (crate : A.crate) : unit = - (* Filter the functions which contain loops *) - let no_loop_funs = - List.filter - (fun f -> not (LlbcAstUtils.fun_decl_has_loops f)) - crate.functions - in - (* Filter the opaque functions *) - let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in - let type_context, fun_context, global_context = - compute_type_fun_global_contexts crate - in - let test_fun (def : A.fun_decl) : unit = - (* 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 synthesize type_context fun_context global_context - def - in - List.iter test_fun no_loop_funs end |