Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 0295fea1 authored by Sylvain Dailler's avatar Sylvain Dailler

Update ce-bench

parent b27a29e0
......@@ -15,49 +15,51 @@ Line 10:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] }
{"others" : {"type" : "Integer" , "val" : "5" } }] }
a = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "4" } }] }
"val" : "5" } }] }
Line 12:
a = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "4" } }] }
"val" : "5" } }] }
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" ,
"val" : "7646" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "-8454" ,
"value" : {"type" : "Integer" , "val" : "68" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "64" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "3162" ,
"value" : {"type" : "Integer" , "val" : "62" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "69" ,
"value" : {"type" : "Integer" , "val" : "71" } },
a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "7646" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "-8454" ,
"value" : {"type" : "Integer" , "val" : "68" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "64" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "3162" ,
"value" : {"type" : "Integer" , "val" : "62" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "69" ,
"value" : {"type" : "Integer" , "val" : "71" } },
old a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
......@@ -66,31 +68,33 @@ Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" ,
"val" : "7646" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "-8454" ,
"value" : {"type" : "Integer" , "val" : "68" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "64" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "3162" ,
"value" : {"type" : "Integer" , "val" : "62" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "69" ,
"value" : {"type" : "Integer" , "val" : "71" } },
a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 32:
old a.length = {"type" : "Integer" ,
"val" : "7646" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "-8454" ,
"value" : {"type" : "Integer" , "val" : "68" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "64" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "3162" ,
"value" : {"type" : "Integer" , "val" : "62" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "69" ,
"value" : {"type" : "Integer" , "val" : "71" } },
old a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
......@@ -125,31 +129,33 @@ Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" ,
"val" : "7646" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "-8454" ,
"value" : {"type" : "Integer" , "val" : "68" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "64" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "3162" ,
"value" : {"type" : "Integer" , "val" : "62" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "69" ,
"value" : {"type" : "Integer" , "val" : "71" } },
a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "7646" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "-8454" ,
"value" : {"type" : "Integer" , "val" : "68" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "64" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "3162" ,
"value" : {"type" : "Integer" , "val" : "62" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "69" ,
"value" : {"type" : "Integer" , "val" : "71" } },
old a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
......
......@@ -15,21 +15,101 @@ Line 10:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "5" } }] }
{"others" : {"type" : "Integer" , "val" : "6" } }] }
a = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "5" } }] }
"val" : "6" } }] }
Line 12:
a = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "5" } }] }
"val" : "6" } }] }
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" ,
"val" : "7211" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "7212" ,
"value" : {"type" : "Integer" , "val" : "156" } }, {"indice" : "7209" ,
"value" : {"type" : "Integer" , "val" : "4075" } }, {"indice" : "3018" ,
"value" : {"type" : "Integer" , "val" : "4590" } }, {"indice" : "-3777" ,
"value" : {"type" : "Integer" , "val" : "3082" } }, {"indice" : "5475" ,
"value" : {"type" : "Integer" , "val" : "5476" } }, {"indice" : "7210" ,
"value" : {"type" : "Integer" , "val" : "-1736" } }, {"indice" : "3019" ,
"value" : {"type" : "Integer" , "val" : "4589" } }, {"indice" : "5476" ,
"value" : {"type" : "Integer" , "val" : "7891" } }, {"indice" : "982" ,
"value" : {"type" : "Integer" , "val" : "4387" } }, {"indice" : "-24" ,
"value" : {"type" : "Integer" , "val" : "6774" } }, {"indice" : "7211" ,
"value" : {"type" : "Integer" , "val" : "155" } }, {"indice" : "13846" ,
"value" : {"type" : "Integer" , "val" : "154" } }, {"indice" : "7208" ,
"value" : {"type" : "Integer" , "val" : "5737" } },
{"others" : {"type" : "Integer" ,
"val" : "4" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "7211" }
old a.elts = {"type" : "Array" ,
"val" : [{"indice" : "7212" , "value" : {"type" : "Integer" ,
"val" : "156" } }, {"indice" : "7209" , "value" : {"type" : "Integer" ,
"val" : "4075" } }, {"indice" : "3018" , "value" : {"type" : "Integer" ,
"val" : "4590" } }, {"indice" : "-3777" , "value" : {"type" : "Integer" ,
"val" : "3082" } }, {"indice" : "5475" , "value" : {"type" : "Integer" ,
"val" : "5476" } }, {"indice" : "7210" , "value" : {"type" : "Integer" ,
"val" : "-1736" } }, {"indice" : "3019" , "value" : {"type" : "Integer" ,
"val" : "4589" } }, {"indice" : "5476" , "value" : {"type" : "Integer" ,
"val" : "7891" } }, {"indice" : "982" , "value" : {"type" : "Integer" ,
"val" : "4387" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
"val" : "6774" } }, {"indice" : "7211" , "value" : {"type" : "Integer" ,
"val" : "155" } }, {"indice" : "13846" , "value" : {"type" : "Integer" ,
"val" : "154" } }, {"indice" : "7208" , "value" : {"type" : "Integer" ,
"val" : "5737" } }, {"others" : {"type" : "Integer" ,
"val" : "4" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" ,
"val" : "7211" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "7212" ,
"value" : {"type" : "Integer" , "val" : "156" } }, {"indice" : "7209" ,
"value" : {"type" : "Integer" , "val" : "4075" } }, {"indice" : "3018" ,
"value" : {"type" : "Integer" , "val" : "4590" } }, {"indice" : "-3777" ,
"value" : {"type" : "Integer" , "val" : "3082" } }, {"indice" : "5475" ,
"value" : {"type" : "Integer" , "val" : "5476" } }, {"indice" : "7210" ,
"value" : {"type" : "Integer" , "val" : "-1736" } }, {"indice" : "3019" ,
"value" : {"type" : "Integer" , "val" : "4589" } }, {"indice" : "5476" ,
"value" : {"type" : "Integer" , "val" : "7891" } }, {"indice" : "982" ,
"value" : {"type" : "Integer" , "val" : "4387" } }, {"indice" : "-24" ,
"value" : {"type" : "Integer" , "val" : "6774" } }, {"indice" : "7211" ,
"value" : {"type" : "Integer" , "val" : "155" } }, {"indice" : "13846" ,
"value" : {"type" : "Integer" , "val" : "154" } }, {"indice" : "7208" ,
"value" : {"type" : "Integer" , "val" : "5737" } },
{"others" : {"type" : "Integer" ,
"val" : "4" } }] }
Line 32:
old a.length = {"type" : "Integer" ,
"val" : "7211" }
old a.elts = {"type" : "Array" ,
"val" : [{"indice" : "7212" , "value" : {"type" : "Integer" ,
"val" : "156" } }, {"indice" : "7209" , "value" : {"type" : "Integer" ,
"val" : "4075" } }, {"indice" : "3018" , "value" : {"type" : "Integer" ,
"val" : "4590" } }, {"indice" : "-3777" , "value" : {"type" : "Integer" ,
"val" : "3082" } }, {"indice" : "5475" , "value" : {"type" : "Integer" ,
"val" : "5476" } }, {"indice" : "7210" , "value" : {"type" : "Integer" ,
"val" : "-1736" } }, {"indice" : "3019" , "value" : {"type" : "Integer" ,
"val" : "4589" } }, {"indice" : "5476" , "value" : {"type" : "Integer" ,
"val" : "7891" } }, {"indice" : "982" , "value" : {"type" : "Integer" ,
"val" : "4387" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
"val" : "6774" } }, {"indice" : "7211" , "value" : {"type" : "Integer" ,
"val" : "155" } }, {"indice" : "13846" , "value" : {"type" : "Integer" ,
"val" : "154" } }, {"indice" : "7208" , "value" : {"type" : "Integer" ,
"val" : "5737" } }, {"others" : {"type" : "Integer" ,
"val" : "4" } }] }
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
......@@ -57,6 +137,46 @@ old a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"val" : "5" } }] }
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" ,
"val" : "7211" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "7212" ,
"value" : {"type" : "Integer" , "val" : "156" } }, {"indice" : "7209" ,
"value" : {"type" : "Integer" , "val" : "4075" } }, {"indice" : "3018" ,
"value" : {"type" : "Integer" , "val" : "4590" } }, {"indice" : "-3777" ,
"value" : {"type" : "Integer" , "val" : "3082" } }, {"indice" : "5475" ,
"value" : {"type" : "Integer" , "val" : "5476" } }, {"indice" : "7210" ,
"value" : {"type" : "Integer" , "val" : "-1736" } }, {"indice" : "3019" ,
"value" : {"type" : "Integer" , "val" : "4589" } }, {"indice" : "5476" ,
"value" : {"type" : "Integer" , "val" : "7891" } }, {"indice" : "982" ,
"value" : {"type" : "Integer" , "val" : "4387" } }, {"indice" : "-24" ,
"value" : {"type" : "Integer" , "val" : "6774" } }, {"indice" : "7211" ,
"value" : {"type" : "Integer" , "val" : "155" } }, {"indice" : "13846" ,
"value" : {"type" : "Integer" , "val" : "154" } }, {"indice" : "7208" ,
"value" : {"type" : "Integer" , "val" : "5737" } },
{"others" : {"type" : "Integer" ,
"val" : "4" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "7211" }
old a.elts = {"type" : "Array" ,
"val" : [{"indice" : "7212" , "value" : {"type" : "Integer" ,
"val" : "156" } }, {"indice" : "7209" , "value" : {"type" : "Integer" ,
"val" : "4075" } }, {"indice" : "3018" , "value" : {"type" : "Integer" ,
"val" : "4590" } }, {"indice" : "-3777" , "value" : {"type" : "Integer" ,
"val" : "3082" } }, {"indice" : "5475" , "value" : {"type" : "Integer" ,
"val" : "5476" } }, {"indice" : "7210" , "value" : {"type" : "Integer" ,
"val" : "-1736" } }, {"indice" : "3019" , "value" : {"type" : "Integer" ,
"val" : "4589" } }, {"indice" : "5476" , "value" : {"type" : "Integer" ,
"val" : "7891" } }, {"indice" : "982" , "value" : {"type" : "Integer" ,
"val" : "4387" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
"val" : "6774" } }, {"indice" : "7211" , "value" : {"type" : "Integer" ,
"val" : "155" } }, {"indice" : "13846" , "value" : {"type" : "Integer" ,
"val" : "154" } }, {"indice" : "7208" , "value" : {"type" : "Integer" ,
"val" : "5737" } }, {"others" : {"type" : "Integer" ,
"val" : "4" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Valid
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
......
......@@ -119,6 +119,12 @@ x = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T64 g9 : Unknown (other)
Counter-example model:File floats.mlw:
Line 47:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x0.0000000000001p-1023" ,
"value" : 0 } }
bench/ce/floats.mlw T64 g10 : Unknown (other)
Counter-example model:File floats.mlw:
Line 49:
......
......@@ -161,4 +161,10 @@ y = {"type" : "Integer" ,
"val" : "1073749692" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Valid
bench/ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Timeout
bench/ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 58:
x = {"type" : "Integer" , "val" : "1073741824" }
y = {"type" : "Integer" ,
"val" : "1073741824" }
......@@ -5,8 +5,10 @@ a.length = {"type" : "Integer" ,
"val" : "0" }
File jlamp_array.mlw:
Line 18:
a.length = {"type" : "Integer" ,
"val" : "0" }
a.length = {"type" : "Integer" , "val" : "0" }
a.elts = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "3" } }] }
bench/ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
Counter-example model:File jlamp_array.mlw:
......@@ -82,7 +84,7 @@ bench/ce/jlamp_array.mlw Array WP_parameter f : Valid
bench/ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
Counter-example model:File jlamp_array.mlw:
Line 18:
a.length = {"type" : "Integer" , "val" : "0" }
a.length = {"type" : "Integer" , "val" : "1" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
......
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