diff --git a/CHANGES.md b/CHANGES.md index 80183edea525dd8106f52259cf1b2de20459a8ab..341c3d92d233d28912e005b5a4b08a5557a3f0be 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -37,6 +37,7 @@ IDE Counterexamples * Field names now use ident names instead of smt generated ones: int32qtint -> int32'int + * Fix parsing of bitvector counterexamples orignated from Z3 Provers * support for Z3 4.8.1 (released Oct 16, 2018) diff --git a/bench/ce/oracles/bv32_Z3,4.6.0_SP.oracle b/bench/ce/oracles/bv32_Z3,4.6.0_SP.oracle index 64597e99a05906ee67e978f4b022f21cfdb0ac2d..5ca806be3eb6022a388b1ccb58c2f832a92f344a 100644 --- a/bench/ce/oracles/bv32_Z3,4.6.0_SP.oracle +++ b/bench/ce/oracles/bv32_Z3,4.6.0_SP.oracle @@ -1,3 +1,47 @@ Strongest Postcondition bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown +Counter-example model:File bv32.mlw: +Line 7: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000022" } }] } } +Line 9: +r, [[@mlw:reference_var], [@introduced], [@field:0:contents], +[@model_trace:r]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000084" } }] } } +Line 10: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000042" } }] } } +Line 11: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000084" } }] } } + bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown +Counter-example model:File bv32.mlw: +Line 13: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000022" } }] } } +Line 15: +r, [[@mlw:reference_var], [@introduced], [@field:0:contents], +[@model_trace:r]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000084" } }] } } +Line 16: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000042" } }] } } +Line 17: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000084" } }] } } + diff --git a/bench/ce/oracles/bv32_Z3,4.6.0_WP.oracle b/bench/ce/oracles/bv32_Z3,4.6.0_WP.oracle index 43b527a9b462f1b1ac6fcf70484f6a1c57644c78..37c3594ea5dcd005a18a0973085721db9e8d2052 100644 --- a/bench/ce/oracles/bv32_Z3,4.6.0_WP.oracle +++ b/bench/ce/oracles/bv32_Z3,4.6.0_WP.oracle @@ -1,3 +1,47 @@ Weakest Precondition bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown +Counter-example model:File bv32.mlw: +Line 7: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000022" } }] } } +Line 9: +r, [[@mlw:reference_var], [@introduced], [@field:0:contents], +[@model_trace:r]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000084" } }] } } +Line 10: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000042" } }] } } +Line 11: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000084" } }] } } + bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown +Counter-example model:File bv32.mlw: +Line 13: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000022" } }] } } +Line 15: +r, [[@mlw:reference_var], [@introduced], [@field:0:contents], +[@model_trace:r]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000084" } }] } } +Line 16: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000042" } }] } } +Line 17: +r, [[@mlw:reference_var], [@introduced], +[@field:0:contents]] = {"type" : "Record" , +"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" , +"val" : "#x00000084" } }] } } + diff --git a/src/driver/collect_data_model.ml b/src/driver/collect_data_model.ml index d8e4ec05691ee36d8e5c03fdc63e26e1c9b1787f..3fb03dcbaf9727b9d44a10f92588cf605893d2fb 100644 --- a/src/driver/collect_data_model.ml +++ b/src/driver/collect_data_model.ml @@ -672,7 +672,8 @@ let create_list (projections_list: Ident.ident Mstr.t) Mstr.fold (fun key value list_acc -> try (convert_to_model_element ~set_str key value :: list_acc) - with Not_value when not (Debug.test_flag Debug.stack_trace) -> list_acc + with Not_value when not (Debug.test_flag Debug.stack_trace) -> + Debug.dprintf debug_cntex "Element creation failed: %s@." key; list_acc | e -> raise e) table [] diff --git a/src/driver/parse_smtv2_model_lexer.mll b/src/driver/parse_smtv2_model_lexer.mll index 0989693e25edd7c31afee6e53d79ec2248d2e3c1..c6a9a00db282ea1db2f01d19169f12cd0b7004b9 100644 --- a/src/driver/parse_smtv2_model_lexer.mll +++ b/src/driver/parse_smtv2_model_lexer.mll @@ -24,7 +24,7 @@ let dec_num = num"."num let name = (['a'-'z']*'_'*['0'-'9']*)* let dummy = ('_''_''_')? let float_num = '#'('b' | 'x') hexa_num - +let bv_num = '#'('b' | 'x') hexa_num rule token = parse | '\n' @@ -73,6 +73,7 @@ rule token = parse | "(_" space+ "NaN" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Not_a_number } | "(fp" space+ (float_num as b) space+ (float_num as eb) space+ (float_num as sb) ")" { FLOAT_VALUE (Model_parser.interp_float b eb sb) } + | bv_num as bv_value { BITVECTOR_VALUE bv_value } | num as integer { INT_STR (integer) }