diff options
| author | Kathy Gray | 2015-07-24 13:52:38 +0100 |
|---|---|---|
| committer | Kathy Gray | 2015-07-24 13:52:38 +0100 |
| commit | 43427019f9f2c1e64a07ec6ee3caef8bd1a5c165 (patch) | |
| tree | 49e029dbd39885e18ea7ecfef2816ba888ad5895 /src/lem_interp | |
| parent | e5083eca71d9d4a1092c4553c6ca448e256e6738 (diff) | |
Turn back off new analysis style until it works
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index d9b089e0..15584b60 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -941,7 +941,11 @@ let env_to_let mode (LEnv _ env) (E_aux e annot) taint_env = (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan)) (E_aux e annot)) annot, taint_env) -end +end +(* +let fix_up_nondet typ branches annot = + match typ with + | T_id "unit" -> *) (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *) val match_pattern : top_level -> pat tannot -> value -> bool * bool * lenv @@ -1375,7 +1379,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | (V_vector _ _ [(V_lit(L_aux L_one _))],true) -> interp_main mode t_level l_env lm thn | (V_vector _ _ [(V_lit(L_aux L_one _))],false) -> debug_out Nothing Nothing thn t_level lm l_env | (V_unknown,_) -> - interp_main mode t_level l_env lm (E_aux (E_nondet [thn;els]) (l,(non_det_annot annot))) + interp_main mode t_level l_env lm (E_aux (E_block [thn;els]) (l,annot)) | (_,true) -> interp_main mode t_level l_env lm els | (_,false) -> debug_out Nothing Nothing els t_level lm l_env end) (fun a -> update_stack a (add_to_top_frame (fun c env -> (E_aux (E_if c thn els) (l,annot), env)))) @@ -1467,7 +1471,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = let (lets,taint_env) = List.foldr (fun (env,_,exp) (rst,taint_env) -> let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in - interp_main mode t_level taint_env lm (E_aux (E_nondet lets) (l,(non_det_annot annot))) + interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot)) end) (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_case e pats) (l,annot), env)))) | E_record(FES_aux (FES_Fexps fexps _) fes_annot) -> @@ -1874,7 +1878,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = let (lets,taint_env) = List.foldr (fun (env,_,exp) (rst,taint_env) -> let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in - interp_main mode t_level taint_env lm (E_aux (E_nondet lets) (l,(non_det_annot annot))) + interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot)) end) | Nothing -> (Error l (String.stringAppend "Internal error: function with tag global unfound " name),lm,le) end) |