Commit 5faead25 authored by Sylvain Dailler's avatar Sylvain Dailler

ce: Correctly remove proxy variables from counterexamples

parent db9b0d9b
Pipeline #55038 passed with stages
in 42 minutes
......@@ -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