Commit 6b4fa6f2 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'ce_no_proxy' into 'master'

ce: Correctly remove proxy variables from counterexamples

See merge request !77
parents db9b0d9b 5faead25
Pipeline #55042 passed with stages
in 49 minutes and 8 seconds
......@@ -7,10 +7,6 @@ a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "127" } }
File jlamp_projections.mlw:
Line 15:
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 29:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "127" } }
......@@ -18,17 +14,10 @@ Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 15:
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 41:
b, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
......@@ -41,7 +30,4 @@ b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
......@@ -7,10 +7,6 @@ a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "127" } }
File jlamp_projections.mlw:
Line 15:
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 29:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "127" } }
......@@ -18,17 +14,10 @@ Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "127" } }
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Timeout or Unknown
Counter-example model:File jlamp_projections.mlw:
Line 15:
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 41:
b, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
......@@ -41,7 +30,4 @@ b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "127" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
......@@ -7,10 +7,6 @@ a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
File jlamp_projections.mlw:
Line 15:
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 29:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "0" } }
......@@ -18,17 +14,10 @@ Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (sat)
Counter-example model:File jlamp_projections.mlw:
Line 15:
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 41:
b, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
......@@ -41,7 +30,4 @@ b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
......@@ -7,10 +7,6 @@ a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
File jlamp_projections.mlw:
Line 15:
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 29:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "0" } }
......@@ -18,17 +14,10 @@ Line 30:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (sat)
Counter-example model:File jlamp_projections.mlw:
Line 15:
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
Line 41:
b, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "f" , "value" : {"proj_name" : "to_int1" ,
......@@ -41,7 +30,4 @@ b, [[@introduced], [@model_trace:b]] = {"type" : "Record" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } } },
{"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : true } }] } }
o, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
......@@ -131,8 +131,8 @@ let update_info_labels lsname cur_attrs t ls =
let check_for_counterexample t =
let is_app t =
match t.t_node with
| Tapp (_, []) -> true
| Tapp (ls, []) -> not (Sattr.mem proxy_attr ls.ls_name.id_attrs)
| _ -> false
in
Sattr.for_all (fun a -> not (attr_equal proxy_attr a)) t.t_attrs &&
not (Sattr.mem proxy_attr t.t_attrs) &&
t.t_loc <> None && (is_app t)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment