Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test @ df647a81

Name Size Revision Age Author Comment
Makefile 244 Bytes b8ae1bbc about 7 years Pierre-Loïc Garoche Improvements as suggested by e. Noulard: better...
test-compile.sh 5.42 KB c518d082 about 7 years Xavier Thirioux - added generation of clock information in inte...
tests_ok.list 89.2 KB df647a81 almost 7 years Guillaume Davy First commit in acsl proof branch

Latest revisions

# Date Author Comment
df647a81 05/06/2014 03:01 PM Guillaume Davy

First commit in acsl proof branch
701b0c0a 03/17/2014 07:44 AM Pierre-Loïc Garoche

Moved tests outside of source code to avoid useless duplication.
96fecb0f 03/12/2014 05:59 PM Pierre-Loïc Garoche

Lots of changes: mainly solved bugs
- specification is now stored as a set of equations
- the tuple splitting is performed during normalization and not anymore in machine code
- solved bug with tuple equalities, ie. x = (a,b,c) = (c,d,e)
- better handling of acsl generation including quantifiers...
26031546 03/11/2014 11:41 PM Pierre-Loïc Garoche

Merged trunk modifs up to r186.
5eded996 03/11/2014 01:42 AM Pierre-Loïc Garoche

Ongoing work on specification compilation

- Integrated changes of trunk
- changed the types of extended expressions: only allow prenex forms
- normalization and machine code extended to deal with compilation of spec
- other annotations are almost not considered yet....
6bab3787 03/05/2014 02:35 PM Xavier Thirioux

In order to export any type of constants, moved type definitions from .c to .h
3e79b3a5 03/01/2014 03:38 PM Xavier Thirioux

- stupid svn had removed a file, again
c518d082 03/01/2014 03:37 PM Xavier Thirioux

- added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files
626e6f03 02/28/2014 11:59 PM Pierre-Loïc Garoche

Updated script. Does not seem to be fully functional yet.
3e36d4e0 02/28/2014 11:59 PM Pierre-Loïc Garoche

Added default ensures statements

View revisions

Also available in: Atom