Project

General

Profile

Revision f5c36991 TODO.org

View differences:

TODO.org
29 29
** clock calculus
30 30
*** extension from named clocks to valued clocks ?
31 31
*** static inputs should be polymorphic, as global constants are: done
32
* TODO Revalidation of k-inductive properties at code level
33
We identified the following items to be taken care of to reach the fully
34
working prototype
35
** How to access to ACSL datatypes and printers
36
*** Problematics
37
we have to choose one of those options or create a new one
38
**** option1 (ugly)
39
     - link directly with the cmx in /usr/loca/share/framac
40
     - see example
41
     - problem with namespace (all framac modules may conflict with lustrec
42
       modules)
43
     - but good option to start to code (access to types and printers)
44
**** option 2: create a standalone framac.cmxa archive file
45
     - requires to compile frama-c with -pack framac
46
     - problem today with framac compilation
47
     - meeting with CEA to see if they want to add this feature
48
**** option3: as a plugin of frama-c
49
     - depending on the configure option, create one or two tools
50
       - lustrec without annotations (current version)
51
       - lustrec with ACSL as a frama-c plugin
52
	 eg. frama-c -lustrec args ....
53
     - question on the entry point: single bash script that, depending on
54
       options, redirects to the binary or the framac plugin
55
** Compilation of lustre nodes as ACSL predicate
56
*** Problematics
57
   - expressed over pure struct (no pointers, static struct)
58
   - generation of static struct
59
   - generation of init and step (no pointers for output, nor mem state)
60
     step(in, out, memstate_before, memstate_after)
61
**** how do to it properly
62
     - for the moment it is a sort of hack within the C backend
63
     - shoudln't it be more like a specific ACSL backend that will be evaluated
64
       only on selected nodes
65
     - for example a frama-c plugin could call the "compiler" twice, 
66
       - one to generate an ACSL encoding for (all|a selection of) nodes
67
       - one to generate annotated C code, knowing that those predicates init
68
         and step and static struct exist
69

  
70

  
71
** Stateful observers
72
*** Problematics
73
   - generate (ghost) code to express the memories as additional (ghost) fields
74
     of the node struct
75
   - introduce (ghost) code update for those memories
76
    
77
     
78
** Relationship between pointer based struct and static struct
79
** Annotation of C instructions with live variables (as in optim/*.c files)
80
*** Problematics
81
   - while iterating through scheduled list of instructions, introduce the
82
     assert predicate_X; and keep its definition in an environement.
83
   - this env of predicate has to be printed in the header of the source file
84
   - need the support of Xavier for that (clocks related stuff)
85
   - xavier, does it need to be done while doing the dead variables analysis ?
86
     I (pl) undertood that it was independant and generic
87
** Prove the ACSL predicate Pre and Post as k-inductive wrt predicates Init and Step 

Also available in: Unified diff