Experiment a bit with Jessie3.

src/jessie/ACSLtoWhy3.ml

@@ -664,12 +664,13 @@ let binop op e1 e2 =
   let ls,ty =
     match op with
       | PlusA -> add_int, Mlw_ty.ity_int
+      | MinusA -> sub_int, Mlw_ty.ity_int
       | Mult -> mul_int, Mlw_ty.ity_int
       | Lt -> lt_int, Mlw_ty.ity_bool
       | Le -> le_int, Mlw_ty.ity_bool
       | Gt | Ge | Eq | Ne ->
         Self.not_yet_implemented "binop comp"
-      | PlusPI|IndexPI|MinusA|MinusPI|MinusPP ->
+      | PlusPI|IndexPI|MinusPI|MinusPP ->
         Self.not_yet_implemented "binop plus/minus"
       | Div|Mod ->
         Self.not_yet_implemented "binop div/mod"

src/jessie/Makefile.in

-
 FRAMAC_SHARE    := $(shell frama-c -print-path)
 FRAMAC_LIBDIR   := $(shell frama-c -print-libpath)
 PLUGIN_NAME     := Jessie3
@@ -6,22 +5,20 @@ PLUGIN_CMO      := literals ACSLtoWhy3 register
 
 SHELL := /bin/bash
 
-ifeq (@enable_local@,yes)
 WHYLIB := ../../lib/why3
-else
-WHYLIB := @OCAMLLIB@/why3
-endif
 
-PLUGIN_EXTRA_BYTE:= $(WHYLIB)/why3.cma 
+PLUGIN_EXTRA_BYTE:= $(WHYLIB)/why3.cma
 PLUGIN_EXTRA_OPT:= $(WHYLIB)/why3.cmxa
 PLUGIN_BFLAGS:= -I $(WHYLIB)
 PLUGIN_OFLAGS:= -I $(WHYLIB)
-PLUGIN_LINK_BFLAGS:= -I $(WHYLIB) 
+PLUGIN_LINK_BFLAGS:= -I $(WHYLIB)
 PLUGIN_LINK_OFLAGS:= -I $(WHYLIB)
 PLUGIN_TESTS_DIRS := basic
 
+OCAMLLEX  = @OCAMLLEX@
+
 literals.ml: literals.mll
-	ocamllex $<
+	$(OCAMLLEX) $<
 
 include $(FRAMAC_SHARE)/Makefile.dynamic