Skip to content
GitLab
Commit a78ed907 authored by David Hauzar's avatar David Hauzar
Browse files

Merge branch 'master' into counter-examples 

Conflicts:
	src/ide/gmain.ml
parents 59a46a0e efa3dbcd
Expand all Hide whitespace changes
Inline Side-by-side
.gitignore
View file @ a78ed907
......@@ -263,15 +263,11 @@ pvsbin/
# jessie3
/src/jessie/.depend
/src/jessie/Jessie3_DEP
/src/jessie/autom4te.cache/
/src/jessie/config.log
/src/jessie/config.status
/src/jessie/Makefile
/src/jessie/literals.ml
/src/jessie/ptests_local_config.ml
/src/jessie/tests/basic/frama_c_journal.ml
/src/jessie/tests/ptests_config
/src/jessie/tests/basic/result/*.log
/src/jessie/tests/demo/result/*.log
/trash
Makefile.in
View file @ a78ed907
......@@ -1278,8 +1278,8 @@ CLEANLIBS += lib/why3/why3extract
ifeq (@enable_frama_c@,yes)
byte: jessie.byte
opt: jessie.opt
nobyte: jessie.byte
noopt: jessie.opt
jessie.byte: src/jessie/Makefile lib/why3/why3.cma
@$(MAKE) -C src/jessie Jessie3.cma
......
configure.in
View file @ a78ed907
......@@ -677,10 +677,10 @@ if test "$enable_frama_c" = yes ; then
FRAMAC_VERSION=`$FRAMAC -version | sed -n -e 's|Version: *\(.*\)$|\1|p'`
AC_MSG_RESULT($FRAMAC_VERSION)
case $FRAMAC_VERSION in
Neon-*) ;;
*) AC_MSG_WARN(Version Neon required.)
Sodium-*) ;;
*) AC_MSG_WARN(Version Sodium required.)
enable_frama_c=no
reason_frama_c=" (version Neon required)"
reason_frama_c=" (version Sodium required)"
;;
esac
FRAMAC_SHARE=`$FRAMAC -print-path`
......
drivers/cvc4_14.drv
View file @ a78ed907
......@@ -13,6 +13,7 @@ prelude "(set-logic AUFBVDTNIRA)"
*)
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "discrimination.gen"
transformation "inline_trivial"
......
drivers/isabelle.drv
View file @ a78ed907
......@@ -8,3 +8,5 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
transformation "simplify_trivial_quantification_in_goal"
drivers/smt-libv2-bv.gen 0 → 100644
View file @ a78ed907
(* Why3 driver for SMT-LIB2, common part of bit-vector theories *)
prelude ";;; SMT-LIB2 driver: bit-vectors, common part"
theory bitvec.BVConverter_32_64
syntax function toBig "((_ zero_extend 32) %1)"
syntax function toSmall "((_ extract 31 0) %1)"
end
theory bitvec.BVConverter_16_64
syntax function toBig "((_ zero_extend 48) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
end
theory bitvec.BVConverter_8_64
syntax function toBig "((_ zero_extend 56) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bitvec.BVConverter_16_32
syntax function toBig "((_ zero_extend 16) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
end
theory bitvec.BVConverter_8_32
syntax function toBig "((_ zero_extend 24) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bitvec.BVConverter_8_16
syntax function toBig "((_ zero_extend 8) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bv.BV32
syntax type t "(_ BitVec 32)"
syntax function zero "#x00000000"
syntax function ones "#xFFFFFFFF"
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function sdiv "(bvsdiv %1 %2)"
syntax function srem "(bvsrem %1 %2)"
syntax function smod "(bvsmod %1 %2)"
syntax function rotate_left "((_ rotate_left 1) %1)"
syntax function rotate_right "((_ rotate_right 1) %1)"
syntax function lsr "(bvlshr %1 ((_ int2bv 32) %2))"
syntax function lsl "(bvshl %1 ((_ int2bv 32) %2))"
syntax function asr "(bvashr %1 ((_ int2bv 32) %2))"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax converter of_int_const "((_ int2bv 32) %1)"
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
end
theory bv.BV64
syntax type t "(_ BitVec 64)"
syntax function zero "#x0000000000000000"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function sdiv "(bvsdiv %1 %2)"
syntax function srem "(bvsrem %1 %2)"
syntax function smod "(bvsmod %1 %2)"
syntax function rotate_left "((_ rotate_left 1) %1)"
syntax function rotate_right "((_ rotate_right 1) %1)"
syntax function lsr "(bvlshr %1 ((_ int2bv 64) %2))"
syntax function lsl "(bvshl %1 ((_ int2bv 64) %2))"
syntax function asr "(bvashr %1 ((_ int2bv 64) %2))"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax converter of_int_const "((_ int2bv 64) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
end
theory bv.BV16
syntax type t "(_ BitVec 16)"
syntax function zero "#x0000"
syntax function ones "#xFFFF"
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function sdiv "(bvsdiv %1 %2)"
syntax function srem "(bvsrem %1 %2)"
syntax function smod "(bvsmod %1 %2)"
syntax function rotate_left "((_ rotate_left 1) %1)"
syntax function rotate_right "((_ rotate_right 1) %1)"
syntax function lsr "(bvlshr %1 ((_ int2bv 16) %2))"
syntax function lsl "(bvshl %1 ((_ int2bv 16) %2))"
syntax function asr "(bvashr %1 ((_ int2bv 16) %2))"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax converter of_int_const "((_ int2bv 16) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
end
theory bv.BV8
syntax type t "(_ BitVec 8)"
syntax function zero "#x00"
syntax function ones "#xFF"
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function sdiv "(bvsdiv %1 %2)"
syntax function srem "(bvsrem %1 %2)"
syntax function smod "(bvsmod %1 %2)"
syntax function rotate_left "((_ rotate_left 1) %1)"
syntax function rotate_right "((_ rotate_right 1) %1)"
syntax function lsr "(bvlshr %1 ((_ int2bv 8) %2))"
syntax function lsl "(bvshl %1 ((_ int2bv 8) %2))"
syntax function asr "(bvashr %1 ((_ int2bv 8) %2))"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax converter of_int_const "((_ int2bv 8) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
end
theory bv.BVConverter_32_64
syntax function toBig "((_ zero_extend 32) %1)"
syntax function toSmall "((_ extract 31 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_16_64
syntax function toBig "((_ zero_extend 48) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_8_64
syntax function toBig "((_ zero_extend 56) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_16_32
syntax function toBig "((_ zero_extend 16) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_8_32
syntax function toBig "((_ zero_extend 24) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_8_16
syntax function toBig "((_ zero_extend 8) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
remove prop back_from_bigBV
end
theory bitvec.Pow2int
remove prop Power_0
remove prop Power_s
remove prop Power_1
remove prop Power_sum
remove prop pow2pos
remove prop Div_mult_inst
remove prop Div_double
remove prop Div_pow
remove prop Div_double_neg
remove prop Div_pow2
remove prop Div_div_pow
remove prop Mod_pow2_gen
remove prop pow2_0
remove prop pow2_1
remove prop pow2_2
remove prop pow2_3
remove prop pow2_4
remove prop pow2_5
remove prop pow2_6
remove prop pow2_7
remove prop pow2_8
remove prop pow2_9
remove prop pow2_10
remove prop pow2_11
remove prop pow2_12
remove prop pow2_13
remove prop pow2_14
remove prop pow2_15
remove prop pow2_16
remove prop pow2_17
remove prop pow2_18
remove prop pow2_19
remove prop pow2_20
remove prop pow2_21
remove prop pow2_22
remove prop pow2_23
remove prop pow2_24
remove prop pow2_25
remove prop pow2_26
remove prop pow2_27
remove prop pow2_28
remove prop pow2_29
remove prop pow2_30
remove prop pow2_31
remove prop pow2_32
remove prop pow2_33
remove prop pow2_34
remove prop pow2_35
remove prop pow2_36
remove prop pow2_37
remove prop pow2_38
remove prop pow2_39
remove prop pow2_40
remove prop pow2_41
remove prop pow2_42
remove prop pow2_43
remove prop pow2_44
remove prop pow2_45
remove prop pow2_46
remove prop pow2_47
remove prop pow2_48
remove prop pow2_49
remove prop pow2_50
remove prop pow2_51
remove prop pow2_52
remove prop pow2_53
remove prop pow2_54
remove prop pow2_55
remove prop pow2_56
remove prop pow2_57
remove prop pow2_58
remove prop pow2_59
remove prop pow2_60
remove prop pow2_61
remove prop pow2_62
remove prop pow2_63
remove prop pow2_64
end
drivers/smt-libv2.drv
View file @ a78ed907
......@@ -27,7 +27,7 @@ theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding:ignore_polymorphism_ls" predicate (=)
meta "encoding : kept" type int
end
......@@ -150,325 +150,3 @@ theory map.Map
syntax function set "(store %1 %2 %3)"
(* syntax function const "(const[%t0] %1)" *)
end
theory bitvec.BVConverter_32_64
syntax function toBig "((_ zero_extend 32) %1)"
syntax function toSmall "((_ extract 31 0) %1)"
end
theory bitvec.BVConverter_16_64
syntax function toBig "((_ zero_extend 48) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
end
theory bitvec.BVConverter_8_64
syntax function toBig "((_ zero_extend 56) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bitvec.BVConverter_16_32
syntax function toBig "((_ zero_extend 16) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
end
theory bitvec.BVConverter_8_32
syntax function toBig "((_ zero_extend 24) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bitvec.BVConverter_8_16
syntax function toBig "((_ zero_extend 8) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bv.BV32
syntax type t "(_ BitVec 32)"
syntax function zero "#x00000000"
syntax function ones "#xFFFFFFFF"
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function sdiv "(bvsdiv %1 %2)"
syntax function srem "(bvsrem %1 %2)"
syntax function smod "(bvsmod %1 %2)"
syntax function rotate_left "((_ rotate_left 1) %1)"
syntax function rotate_right "((_ rotate_right 1) %1)"
syntax function lsr "(bvlshr %1 ((_ int2bv 32) %2))"
syntax function lsl "(bvshl %1 ((_ int2bv 32) %2))"
syntax function asr "(bvashr %1 ((_ int2bv 32) %2))"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax converter of_int_const "((_ int2bv 32) %1)"
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
end
theory bv.BV64
syntax type t "(_ BitVec 64)"
syntax function zero "#x0000000000000000"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function sdiv "(bvsdiv %1 %2)"
syntax function srem "(bvsrem %1 %2)"
syntax function smod "(bvsmod %1 %2)"
syntax function rotate_left "((_ rotate_left 1) %1)"
syntax function rotate_right "((_ rotate_right 1) %1)"
syntax function lsr "(bvlshr %1 ((_ int2bv 64) %2))"
syntax function lsl "(bvshl %1 ((_ int2bv 64) %2))"
syntax function asr "(bvashr %1 ((_ int2bv 64) %2))"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax converter of_int_const "((_ int2bv 64) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
end
theory bv.BV16
syntax type t "(_ BitVec 16)"
syntax function zero "#x0000"
syntax function ones "#xFFFF"
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function sdiv "(bvsdiv %1 %2)"
syntax function srem "(bvsrem %1 %2)"
syntax function smod "(bvsmod %1 %2)"
syntax function rotate_left "((_ rotate_left 1) %1)"
syntax function rotate_right "((_ rotate_right 1) %1)"
syntax function lsr "(bvlshr %1 ((_ int2bv 16) %2))"
syntax function lsl "(bvshl %1 ((_ int2bv 16) %2))"
syntax function asr "(bvashr %1 ((_ int2bv 16) %2))"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax converter of_int_const "((_ int2bv 16) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
end
theory bv.BV8
syntax type t "(_ BitVec 8)"
syntax function zero "#x00"
syntax function ones "#xFF"
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function sdiv "(bvsdiv %1 %2)"
syntax function srem "(bvsrem %1 %2)"
syntax function smod "(bvsmod %1 %2)"
syntax function rotate_left "((_ rotate_left 1) %1)"
syntax function rotate_right "((_ rotate_right 1) %1)"
syntax function lsr "(bvlshr %1 ((_ int2bv 8) %2))"
syntax function lsl "(bvshl %1 ((_ int2bv 8) %2))"
syntax function asr "(bvashr %1 ((_ int2bv 8) %2))"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax converter of_int_const "((_ int2bv 8) %1)"
syntax predicate eq "(= %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
end
theory bv.BVConverter_32_64
syntax function toBig "((_ zero_extend 32) %1)"
syntax function toSmall "((_ extract 31 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_16_64
syntax function toBig "((_ zero_extend 48) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_8_64
syntax function toBig "((_ zero_extend 56) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_16_32
syntax function toBig "((_ zero_extend 16) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_8_32
syntax function toBig "((_ zero_extend 24) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
remove prop back_from_bigBV
end
theory bv.BVConverter_8_16
syntax function toBig "((_ zero_extend 8) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
remove prop back_from_bigBV
end
theory bitvec.Pow2int
remove prop Power_0
remove prop Power_s
remove prop Power_1
remove prop Power_sum
remove prop pow2pos
remove prop Div_mult_inst
remove prop Div_double
remove prop Div_pow
remove prop Div_double_neg
remove prop Div_pow2