diff --git a/src/TODO b/src/TODO
index aa0947118bfcec7e09f104d7613f5f104f019dfe..8e2efa754aae0cb5e68eff1ecb3b6c8913949f35 100644
--- a/src/TODO
+++ b/src/TODO
@@ -73,11 +73,8 @@ est evalu
* au sujet des pragma:
- ex : %ASSUME:assumeSelectElementOfRank_inArray_%
- je les ai rajouté (un peu) dans le parseur
- -> 3 shift/reduce conflicts !
- et puis il faut que je les mettre partout -> changer une autre
- regle ? sxIdent ?
+
+J'ai associé les pragma aux identificateurs, et seulement à eux. Est-ce suffisant ?
* autoriser les noeuds (ou fonction) sans corps sans avoir a préciser
diff --git a/src/lxm.ml b/src/lxm.ml
index 988bd61737b24dfaee3666607d9e38d6649905d1..8dca6e090986dcb9da781bdb3511a6f1e321463d 100644
--- a/src/lxm.ml
+++ b/src/lxm.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 28/08/2008 (at 10:28) by Erwan Jahier> *)
+(** Time-stamp: <modified the 01/09/2008 (at 17:03) by jahier> *)
(** Common to lus2lic and lic2loc *)
@@ -9,13 +9,17 @@ let new_line ( lexbuf ) = (
()
)
+(* exported *)
+type pragma = Pragma of string * string
+
(* le type ``lexeme'', string + info source *)
type t = {
_file : string ;
_str : string ;
_line : int ;
_cstart : int ;
- _cend : int
+ _cend : int;
+ _pragma : pragma list
}
let str x = (x._str)
@@ -24,6 +28,7 @@ let line x = (x._line)
let cstart x = (x._cstart)
let cend x = (x._cend)
let file x = x._file
+let pragma x = x._pragma
(* affichage standard: *)
let details lxm = (
Printf.sprintf "in file \"%s\", line %d, col %d to %d, token '%s'"
@@ -51,7 +56,8 @@ let dummy str =
_file = String.concat ", " !Global.infiles ;
_line = 0 ;
_cstart = 0 ;
- _cend = 0
+ _cend = 0 ;
+ _pragma = []
}
let last_lexeme = ref (dummy "")
@@ -66,12 +72,13 @@ let make ( lexbuf ) = (
_file = !Global.current_file;
_line = l;
_cstart = c1 ;
- _cend = c2
+ _cend = c2 ;
+ _pragma = []
};
!last_lexeme
)
-
+let add_pragma lxm pl = { lxm with _pragma = pl }
let make_string ( lexbuf ) =
let lxm = make lexbuf in
{ lxm with _str = String.sub lxm._str 1 ((String.length lxm._str)-2) }
diff --git a/src/lxm.mli b/src/lxm.mli
index 0a40d8e2c4948c012b99a92af9574015553d4084..4d2951cb926f86a2f3d0cb94353b1c6a63befc4f 100644
--- a/src/lxm.mli
+++ b/src/lxm.mli
@@ -1,10 +1,11 @@
-(** Time-stamp: <modified the 30/05/2008 (at 15:42) by Erwan Jahier> *)
+(** Time-stamp: <modified the 01/09/2008 (at 17:04) by jahier> *)
(** Common to lus2lic and lic2loc *)
(** Lexeme *)
type t
+type pragma = Pragma of string * string
val dummy : string -> t
@@ -12,6 +13,7 @@ val str : t -> string
val id : t -> Ident.t
val line : t -> int
val file : t -> string
+val pragma : t -> pragma list
(** column numbers *)
val cstart : t -> int
@@ -31,6 +33,7 @@ val new_line : Lexing.lexbuf -> unit
(* remove the quotes from the string *)
val make_string: Lexing.lexbuf -> t
+val add_pragma : t -> pragma list -> t
(** compiler interface *)
diff --git a/src/parser.mly b/src/parser.mly
index edc868814f994eb07e0adeccc9288f20975bbb30..8650bce8ed1e244452981ff4748a0e3e14649997 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -404,7 +404,7 @@ sxIdentRef :
/* sxIdentifiers and lists */
sxIdent: TK_IDENT sxPragma
- { $1 }
+ { (ParserUtils.make_ident $1 $2) }
;
@@ -533,12 +533,12 @@ sxExtNodeDecl:
sxNodeDecl: sxLocalNode {};
sxLocalNode:
-| TK_NODE sxIdent sxStaticParams sxParams TK_RETURNS sxParams sxPragma sxOptSemicol
+| TK_NODE sxIdent sxStaticParams sxParams TK_RETURNS sxParams sxOptSemicol
sxLocals sxBody sxOptEndNode
- { treat_node_decl true $2 $3 $4 $6 $9 $7 (fst $10) (snd $10) }
-| TK_FUNCTION sxIdent sxStaticParams sxParams TK_RETURNS sxParams sxPragma sxOptSemicol
+ { treat_node_decl true $2 $3 $4 $6 $8 (fst $9) (snd $9) }
+| TK_FUNCTION sxIdent sxStaticParams sxParams TK_RETURNS sxParams sxOptSemicol
sxLocals sxBody sxOptEndNode
- { treat_node_decl false $2 $3 $4 $6 $9 $7 (fst $10) (snd $10) }
+ { treat_node_decl false $2 $3 $4 $6 $8 (fst $9) (snd $9) }
| TK_NODE sxIdent sxStaticParams sxNodeProfileOpt TK_EQ sxEffectiveNode sxOptSemicol
{ treat_node_alias true $2 $3 $4 $6 } ;
| TK_FUNCTION sxIdent sxStaticParams sxNodeProfileOpt TK_EQ sxEffectiveNode sxOptSemicol
@@ -682,8 +682,6 @@ sxBody:
sxEquationList: sxEquation
{ $1 }
- | sxPragma sxEquation
- { $2 }
| sxEquationList sxEquation
{
( (fst $2) @ (fst $1) , (snd $2) @ (snd $1) )
diff --git a/src/parserUtils.ml b/src/parserUtils.ml
index 36d4cf73bdd319fef0960b7b877f1f6b7e4ab497..33384b7c14298b47e35db7a99294b75a8e06a2a2 100644
--- a/src/parserUtils.ml
+++ b/src/parserUtils.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 29/08/2008 (at 09:34) by Erwan Jahier> *)
+(** Time-stamp: <modified the 01/09/2008 (at 16:59) by jahier> *)
@@ -334,12 +334,11 @@ let (treat_node_decl : bool -> Lxm.t -> static_param srcflagged list ->
clocked_ids list (* entrées *) ->
clocked_ids list (* sorties *) ->
clocked_ids list (* locales *) ->
- pragma list ->
(val_exp srcflagged) list (* assserts *) ->
(eq_info srcflagged) list (* liste des equations *) ->
unit
) =
- fun has_memory nlxm statics indefs outdefs locdefs _pragma asserts eqs ->
+ fun has_memory nlxm statics indefs outdefs locdefs asserts eqs ->
let vtable = Hashtbl.create 50 in
let rec (treat_vars : clocked_ids list -> var_nature -> var_info srcflagged list) =
(* Procedure de traitement des in, out ou loc, paramétrée par la [var_nature] *)
@@ -477,4 +476,7 @@ let (threat_slice_start : Lxm.t -> val_exp -> val_exp option -> slice_info srcfl
| _ -> assert false
+let (make_ident : Lxm.t -> pragma list -> Lxm.t) =
+ fun lxm pl ->
+ if pl = [] then lxm else Lxm.add_pragma lxm pl
diff --git a/src/syntaxTreeCore.ml b/src/syntaxTreeCore.ml
index 512d36fbd576f35a2470c3b598980fa8de74a2f4..1732e587df482fedc4ec737beb53ca4b1de9f650 100644
--- a/src/syntaxTreeCore.ml
+++ b/src/syntaxTreeCore.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 29/08/2008 (at 09:33) by Erwan Jahier> *)
+(** Time-stamp: <modified the 01/09/2008 (at 17:03) by jahier> *)
(** (Raw) Abstract syntax tree of source programs. *)
@@ -190,4 +190,3 @@ type item_info =
| TypeInfo of type_info
| NodeInfo of node_info
-type pragma = Pragma of string * string
diff --git a/src/test/should_work/demo/Gyroscope2.lus b/src/test/should_work/demo/Gyroscope2.lus
index fb7c62e8036fcf780c83600b8f93339cc472be0f..105a9058075790cb8338d7581f393f8fa6072553 100644
--- a/src/test/should_work/demo/Gyroscope2.lus
+++ b/src/test/should_work/demo/Gyroscope2.lus
@@ -102,9 +102,10 @@ tel
-node Voter(channels : Valid_ChannelT^4; god : real; delta_to_god : real) returns (vote : real)
+node Voter
%ASSUME:assumeVoter%
-%GUARANTEE:guaranteeVoter%;
+%GUARANTEE:guaranteeVoter%
+(channels : Valid_ChannelT^4; god : real; delta_to_god : real) returns (vote : real);
-- Assumes :
-- true;
-- Guarantees :
@@ -270,13 +271,14 @@ tel
-node Channel(previousOutChannel : Valid_ChannelT^4;
+node Channel
+%ASSUME:assumeChannel%
+%GUARANTEE:guaranteeChannel%
+(previousOutChannel : Valid_ChannelT^4;
nbInChannel : int;
inChannel : Faulty_ChannelT;
delta : real; god : real; delta_to_god : real)
-returns (nextOutChannel : Valid_ChannelT^4; outChannel : Valid_ChannelT)
-%ASSUME:assumeChannel%
-%GUARANTEE:guaranteeChannel%;
+returns (nextOutChannel : Valid_ChannelT^4; outChannel : Valid_ChannelT);
-- Assumes :
-- true;
-- Guarantees :
@@ -308,9 +310,10 @@ let
tel
-node EvaluateAxis(channels : Faulty_ChannelT^4; delta : real; god : real; delta_to_god : real) returns (AxisValue : real)
+node EvaluateAxis
%ASSUME:assumeEvaluateAxis%
-%GUARANTEE:guaranteeEvaluateAxis%;
+%GUARANTEE:guaranteeEvaluateAxis%
+(channels : Faulty_ChannelT^4; delta : real; god : real; delta_to_god : real) returns (AxisValue : real);
-- Assumes :
-- var :
-- NbToFar : int((NbToFar = red<<TooFar;4>>(0,channels,god^4,delta_to_god^4)) and (NbToFar <= 1));
diff --git a/src/test/should_work/lionel/Gyroscope.lus b/src/test/should_work/lionel/Gyroscope.lus
index 555f1e682526355d959921ca02850cfd537faf19..71cd495237af5aef0461a95b05c0d50b464ac39b 100644
--- a/src/test/should_work/lionel/Gyroscope.lus
+++ b/src/test/should_work/lionel/Gyroscope.lus
@@ -48,9 +48,10 @@ tel
-node sum(accu_in : real; elt_in : real) returns (accu_out : real)
+node sum
%ASSUME:assumeSum%
-%GUARANTEE:guaranteeSum%;
+%GUARANTEE:guaranteeSum%
+(accu_in : real; elt_in : real) returns (accu_out : real);
let
accu_out = (accu_in + elt_in);
tel
@@ -85,9 +86,10 @@ let
tel
-node Voter(channels : Valid_ChannelT^4; god : real; delta_to_god : real) returns (vote : real)
+node Voter
%ASSUME:assumeVoter%
-%GUARANTEE:guaranteeVoter%;
+%GUARANTEE:guaranteeVoter%
+(channels : Valid_ChannelT^4; god : real; delta_to_god : real) returns (vote : real);
var globalSum : real; nbValid : real; mask : real^4;
let
nbValid = countValidChannels(channels);
@@ -121,9 +123,10 @@ let
tel
-node Channel(inChannel : Faulty_ChannelT; delta : real; god : real; delta_to_god : real) returns (outChannel : Valid_ChannelT)
+node Channel
%ASSUME:assumeChannel%
-%ASSUME:guaranteeChannel%;
+%ASSUME:guaranteeChannel%
+(inChannel : Faulty_ChannelT; delta : real; god : real; delta_to_god : real) returns (outChannel : Valid_ChannelT);
var maintain : bool;
let
-- Il faut se servir de l'utilitaire Maintain:
@@ -178,9 +181,10 @@ let
tel
-node EvaluateAxis(channels : Faulty_ChannelT^4; delta : real; god : real; delta_to_god : real) returns (AxisValue : real)
+node EvaluateAxis
%ASSUME:assumeEvaluateAxis%
-%GUARANTEE:guaranteeEvaluateAxis%;
+%GUARANTEE:guaranteeEvaluateAxis%
+(channels : Faulty_ChannelT^4; delta : real; god : real; delta_to_god : real) returns (AxisValue : real);
var resChannels : Valid_ChannelT^4;
AxisValue2 : real;
let
diff --git a/src/test/should_work/packEnvTest/contractForElementSelectionInArray/packageTableau.lus b/src/test/should_work/packEnvTest/contractForElementSelectionInArray/packageTableau.lus
index 1fad9fe296103bec7129b32bfc4bee605d77ebc3..abead384062403fa3862533099a8dc4e55882f85 100644
--- a/src/test/should_work/packEnvTest/contractForElementSelectionInArray/packageTableau.lus
+++ b/src/test/should_work/packEnvTest/contractForElementSelectionInArray/packageTableau.lus
@@ -89,9 +89,10 @@ tel
-- noeud de selection d'un element dans un tableau
-- assume : rankToSelect>=0
-- guarantee : _isElementOf_(elementSelected, array);
-node selectElementOfRank_inArray_(rankToSelect : int;array : arrayType) returns (elementSelected : elementType)
+node selectElementOfRank_inArray_
%ASSUME:assumeSelectElementOfRank_inArray_%
%GUARANTEE:guaranteeSelectElementOfRank_inArray_%
+(rankToSelect : int;array : arrayType) returns (elementSelected : elementType)
var iterationResult : iteratedStruct;
let
iterationResult = red<<selectOneStage, size>>(iteratedStruct{currentRank = 0; rankToSelect = rankToSelect; elementSelected = array[0]}, array);