Commit ab594372 authored by MARCHE Claude's avatar MARCHE Claude

Jessie3: giving up, Mlw API not enough documented

parent 71ff2e9c
......@@ -483,15 +483,21 @@ let identified_proposition p =
let program_vars = Hashtbl.create 257
let any _ty = Mlw_expr.e_int_const "0000" (* TODO : ref *)
let any _ty =
Mlw_expr.e_const (Term.ConstInt (Term.int_const_decimal "0"))
let create_var v =
let id = Ident.id_fresh v.vname in
let ty = Mlw_ty.vty_value (ctype v.vtype) in
let specialize_ref = Mlw_dty.specialize_psymbol ref_fun in
let vty =
match Mlw_dty.vty_of_dvty specialize_ref with
| Mlw_ty.VTarrow vty -> vty
| Mlw_ty.VTvalue _ -> assert false
in
let def =
Mlw_expr.e_app
(Mlw_expr.e_arrow ref_fun
(Mlw_ty.vty_arrow [] (Mlw_ty.VTvalue ty)))
Mlw_expr.e_app
(Mlw_expr.e_arrow ref_fun vty)
[any ty]
in
let let_defn = Mlw_expr.create_let_defn id def in
......
FRAMAC_SHARE :=$(shell frama-c -print-path)
FRAMAC_LIBDIR :=$(shell frama-c -print-libpath)
FRAMAC_SHARE := $(shell frama-c -print-path)
FRAMAC_LIBDIR := $(shell frama-c -print-libpath)
PLUGIN_NAME := Jessie3
PLUGIN_CMO := literals ACSLtoWhy3 register
SHELL := /bin/bash
PLUGIN_EXTRA_BYTE:= @OCAMLLIB@/why3/why3.cma
PLUGIN_EXTRA_OPT:= @OCAMLLIB@/why3/why3.cmxa
PLUGIN_BFLAGS:= -I +why3
PLUGIN_OFLAGS:= -I +why3
PLUGIN_LINK_BFLAGS:= -I +why3
PLUGIN_LINK_OFLAGS:= -I +why3
ifeq (@enable_local@,yes)
WHYLIB := ../../lib/why3
else
WHYLIB := @OCAMLLIB@/why3
endif
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_OFLAGS:= -I $(WHYLIB)
PLUGIN_TESTS_DIRS := basic
literals.ml: literals.mll
......
......@@ -4,6 +4,13 @@
[jessie3] processing function f
[jessie3] processing function g
[kernel] The full backtrace is:
Raised at file "src/whyml/mlw_ty.ml", line 886, characters 26-29
Called from file "ACSLtoWhy3.ml", line 496, characters 9-50
Called from file "list.ml", line 57, characters 20-23
Called from file "ACSLtoWhy3.ml", line 692, characters 4-55
Called from file "ACSLtoWhy3.ml", line 727, characters 14-26
Called from file "list.ml", line 86, characters 24-34
Called from file "ACSLtoWhy3.ml", line 792, characters 6-48
Called from file "register.ml", line 69, characters 17-37
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
......
......@@ -3,6 +3,13 @@
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] processing function f
[kernel] The full backtrace is:
Raised at file "src/whyml/mlw_ty.ml", line 886, characters 26-29
Called from file "ACSLtoWhy3.ml", line 496, characters 9-50
Called from file "list.ml", line 57, characters 20-23
Called from file "ACSLtoWhy3.ml", line 692, characters 4-55
Called from file "ACSLtoWhy3.ml", line 727, characters 14-26
Called from file "list.ml", line 86, characters 24-34
Called from file "ACSLtoWhy3.ml", line 792, characters 6-48
Called from file "register.ml", line 69, characters 17-37
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
......
......@@ -4,6 +4,13 @@
[jessie3] creating logic symbol 739 (sqr)
[jessie3] processing function isqrt
[kernel] The full backtrace is:
Raised at file "src/whyml/mlw_ty.ml", line 886, characters 26-29
Called from file "ACSLtoWhy3.ml", line 496, characters 9-50
Called from file "list.ml", line 57, characters 20-23
Called from file "ACSLtoWhy3.ml", line 692, characters 4-55
Called from file "ACSLtoWhy3.ml", line 727, characters 14-26
Called from file "list.ml", line 86, characters 24-34
Called from file "ACSLtoWhy3.ml", line 792, characters 6-48
Called from file "register.ml", line 69, characters 17-37
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
......
......@@ -18,7 +18,7 @@ open Mlw_ty.T
(** program/logic symbols *)
(* plymbols represent algebraic type constructors and projections.
(* plsymbols represent algebraic type constructors and projections.
They must be fully applied and the result is equal to the application of
the lsymbol. We need this kind of symbols to cover nullary constructors,
such as Nil, which cannot be given a post-condition. They cannot be
......@@ -181,6 +181,7 @@ val e_label_copy : expr -> expr -> expr
val e_value : pvsymbol -> expr
val e_arrow : psymbol -> vty_arrow -> expr
(** DOCUMENTATION NEEDED PLEASE *)
exception ValueExpected of expr
exception ArrowExpected of expr
......
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