diff --git a/.gitignore b/.gitignore index ae9ce14ded43bd66a842d81baac4a7c6d0d42261..4dcc8d3a715762e6c911bffe4a39f160b5973da3 100644 --- a/.gitignore +++ b/.gitignore @@ -204,5 +204,6 @@ pvsbin/ /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/result/*.log diff --git a/src/jessie/ACSLtoWhy3.ml b/src/jessie/ACSLtoWhy3.ml index 61f6fdead2b1eddcdf3b8efe678050c72f7121ac..813617ab6327f992824f5a3e5047c9d863a2f033 100644 --- a/src/jessie/ACSLtoWhy3.ml +++ b/src/jessie/ACSLtoWhy3.ml @@ -94,6 +94,13 @@ let ref_type : Mlw_ty.T.itysymbol = | Mlw_module.PT itys -> itys | Mlw_module.TS _ -> assert false +let ref_fun : Mlw_expr.psymbol = + match + Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["ref"] + with + | Mlw_module.PS p -> p + | _ -> assert false + (*********) (* types *) @@ -163,15 +170,12 @@ let rec logic_type ty = let constant c = match c with - | Integer(_value,Some s) -> Term.ConstInt (Term.IConstDecimal s) + | Integer(_value,Some s) -> + let c = Literals.integer s in Term.ConstInt c | Integer(_value,None) -> Self.not_yet_implemented "constant Integer None" | LReal(_value,s) -> - (* FIXME *) - if s = "0.0" then - Term.ConstReal (Term.RConstDecimal ("0","0",None)) - else - Self.not_yet_implemented "constant LReal" + let c = Literals.floating_point s in Term.ConstReal c | (LStr _|LWStr _|LChr _|LEnum _) -> Self.not_yet_implemented "constant" @@ -483,7 +487,13 @@ let any _ty = Mlw_expr.e_int_const "0000" (* TODO : ref *) let create_var v = let id = Ident.id_fresh v.vname in let ty = Mlw_ty.vty_value (ctype v.vtype) in - let let_defn = Mlw_expr.create_let_defn id (any ty) in + let def = + Mlw_expr.e_app + (Mlw_expr.e_arrow ref_fun + (Mlw_ty.vty_arrow [] (Mlw_ty.VTvalue ty))) + [any ty] + in + let let_defn = Mlw_expr.create_let_defn id def in let vs = match let_defn.Mlw_expr.let_sym with | Mlw_expr.LetV vs -> vs | Mlw_expr.LetA _ -> assert false diff --git a/src/jessie/Makefile.in b/src/jessie/Makefile.in index c882ff99d57e6b0769dd2c5eb6c8102d067a216e..8e823e6c2a75cc241163bf2f35c390ef1000bf76 100644 --- a/src/jessie/Makefile.in +++ b/src/jessie/Makefile.in @@ -2,7 +2,7 @@ FRAMAC_SHARE :=$(shell frama-c -print-path) FRAMAC_LIBDIR :=$(shell frama-c -print-libpath) PLUGIN_NAME := Jessie3 -PLUGIN_CMO := ACSLtoWhy3 register +PLUGIN_CMO := literals ACSLtoWhy3 register SHELL := /bin/bash @@ -14,6 +14,9 @@ PLUGIN_LINK_BFLAGS:= -I +why3 PLUGIN_LINK_OFLAGS:= -I +why3 PLUGIN_TESTS_DIRS := basic +literals.ml: literals.mll + ocamllex $< + include $(FRAMAC_SHARE)/Makefile.dynamic tests:: diff --git a/src/jessie/literals.mll b/src/jessie/literals.mll new file mode 100644 index 0000000000000000000000000000000000000000..6ae294139d5e945271652cc1b871b01d753bbfc7 --- /dev/null +++ b/src/jessie/literals.mll @@ -0,0 +1,169 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2012 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* INRIA (Institut National de Recherche en Informatique et en *) +(* Automatique) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +{ + + open Why3 + +(* + let int_of_digit chr = + match chr with + '0'..'9' -> (Char.code chr) - (Char.code '0') + | 'a'..'f' -> (Char.code chr) - (Char.code 'a') + 10 + | 'A'..'F' -> (Char.code chr) - (Char.code 'A') + 10 + | _ -> assert false +*) + + + let remove_leading_plus s = + let n = String.length s in + if n > 0 && s.[0] = '+' then String.sub s 1 (n-1) else s + +} + +let rD = ['0'-'9'] +let rO = ['0'-'7'] +let rH = ['a'-'f' 'A'-'F' '0'-'9'] +let rFS = ('f'|'F'|'l'|'L')? +let rIS = ('u'|'U'|'l'|'L')* + +(* +let hex_escape = '\\' ['x' 'X'] rH+ +let oct_escape = '\\' rO rO? rO? +*) + +(* integer literals, both decimal, hexadecimal and octal *) +rule integer_literal = parse + (* hexadecimal *) + | '0'['x''X'] (rH+ as d) rIS eof { Term.IConstHexa d } + (* octal *) + | '0' (rO+ as d) rIS eof { Term.IConstOctal d } + (* decimal *) + | (rD+ as d) rIS eof { Term.IConstDecimal d } +(* TODO: character literals + | ('L'? "'" as prelude) (([^ '\\' '\'' '\n']|("\\"[^ '\n']))+ as content) "'" + { + let b = Buffer.create 5 in + Buffer.add_string b prelude; + let lbf = Lexing.from_string content in + CONSTANT (IntConstant (chr b lbf ^ "'")) + } +*) + | eof { invalid_arg "integer_literal: empty string" } + | _ as c { invalid_arg ("integer_literal: character '" ^ + String.make 1 c ^ "'") } + +(* floating-point literals, both decimal and hexadecimal *) +and floating_point_literal = parse + (* decimal *) + | ( (rD+ as i) ("" as f) ['e' 'E'] (['-' '+']? rD+ as e) + | (rD+ as i) '.' (rD* as f) (['e' 'E'] (['-' '+']? rD+ as e))? + | (rD* as i) '.' (rD+ as f) (['e' 'E'] (['-' '+']? rD+ as e))? ) + rFS eof + { Term.RConstDecimal (i, f, Opt.map remove_leading_plus e) } + + (* hexadecimal *) + | '0'['x''X'] ( (rH* as i) '.' (rH+ as f) + | (rH+ as i) '.' (rH* as f) + | (rH+ as i) ("" as f) ) + ['p''P'] (('-' rD+) as e | '+'? (rD+ as e) ) + rFS eof + { Term.RConstHexa(i, f, e) } + + | eof { invalid_arg "floating_point_literal: empty string" } + | _ as c { invalid_arg ("floating_point_literal: character '" ^ + String.make 1 c ^ "'") } + + +(* TODO ? +and string_literal = parse + | 'L'? '"' as prelude (([^ '\\' '"' '\n']|("\\"[^ '\n']))* as content) '"' + { STRING_LITERAL (prelude.[0] = 'L',content) } +*) + +(* +and chr buffer = parse + | hex_escape + { let s = lexeme lexbuf in + let real_s = String.sub s 2 (String.length s - 2) in + let rec add_one_char s = + let l = String.length s in + if l = 0 then () + else + let h = int_of_digit s.[0] in + let c,s = + if l = 1 then (h,"") + else + (16*h + int_of_digit s.[1], + String.sub s 2 (String.length s - 2)) + in + Buffer.add_char buffer (Char.chr c); add_one_char s + in add_one_char real_s; chr buffer lexbuf + } + | oct_escape + { let s = lexeme lexbuf in + let real_s = String.sub s 1 (String.length s - 1) in + let rec value i s = + if s = "" then i + else value (8*i+int_of_digit s.[0]) + (String.sub s 1 (String.length s -1)) + in let c = value 0 real_s in + Buffer.add_char buffer (Char.chr c); chr buffer lexbuf + } + | escape + { Buffer.add_char buffer + (match (lexeme lexbuf).[1] with + 'a' -> '\007' + | 'b' -> '\b' + | 'f' -> '\012' + | 'n' -> '\n' + | 'r' -> '\r' + | 't' -> '\t' + | '\'' -> '\'' + | '"' -> '"' + | '?' -> '?' + | '\\' -> '\\' + | _ -> assert false + ); chr buffer lexbuf} + | eof { Buffer.contents buffer } + | _ { Buffer.add_string buffer (lexeme lexbuf); chr buffer lexbuf } +*) + + +{ + +let integer s = + let b = Lexing.from_string s in integer_literal b + +let floating_point s = + let b = Lexing.from_string s in floating_point_literal b + + +} + +(* +Local Variables: +compile-command: "make -C ." +End: +*) diff --git a/src/jessie/tests/basic/constants.c b/src/jessie/tests/basic/constants.c new file mode 100644 index 0000000000000000000000000000000000000000..84b7bb1b07308468e2450819581368623749fdda --- /dev/null +++ b/src/jessie/tests/basic/constants.c @@ -0,0 +1,19 @@ +/* run.config + OPT: -journal-disable -jessie3 +*/ + + +/*@ lemma test1 : 2 + 0xa == 0xc; + @*/ + +/*@ lemma test2 : 0.0 + 1.1 == 1.1; + @*/ + + +/* +Local Variables: +compile-command: "frama-c -add-path ../.. -jessie3 constants.c" +End: +*/ + +