21 Commits

Author SHA1 Message Date
Jean-Christophe Filliatre
42c2e450b9 Python/micro-C: at/old/labels now supported
makes use of auto-dereference
2019-07-06 14:54:56 +02:00
Jean-Christophe Filliatre
c8a111a2ec Python/micro-C: at/old/labels not yet supported 2019-07-06 12:41:28 +02:00
Jean-Christophe Filliatre
334aa9bc83 python: fixed call to a function with no argument 2019-07-06 12:09:08 +02:00
Jean-Christophe Filliatre
1bf178c8eb python: support for 'for x in range(i,j)' 2017-02-02 21:52:15 +01:00
Jean-Christophe Filliatre
820c7bbd1e python: fixed for loop 2017-01-31 22:56:00 +01:00
Jean-Christophe Filliatre
de593c3543 python: new example sort 2017-01-31 22:23:15 +01:00
Jean-Christophe Filliatre
0471539784 python: support for return statement 2017-01-31 20:52:16 +01:00
Jean-Christophe Filliatre
e9883d12f7 python: support for procedures (i.e. functions with no return) 2017-01-31 20:19:55 +01:00
Jean-Christophe Filliatre
c5d557018e python: support for break in while loops 2017-01-31 16:02:44 +01:00
Jean-Christophe Filliatre
20cdd1882e python: support for elif 2017-01-31 14:35:51 +01:00
Jean-Christophe Filliatre
e01493e5fc python: support for randint 2017-01-30 22:58:38 +01:00
Jean-Christophe Filliatre
b65d100c56 python: building lists 2017-01-30 22:53:30 +01:00
Jean-Christophe Filliatre
dadb290880 python: division and modulus, fixed for loop 2017-01-30 21:27:16 +01:00
Jean-Christophe Filliatre
17487845c3 python: lists modelled with array 'a instead of ref seq 'a 2017-01-30 19:12:37 +01:00
Jean-Christophe Filliatre
cf8b8e3d57 python: more annotations 2017-01-30 13:50:18 +01:00
Jean-Christophe Filliatre
041f9bafd4 python: lists 2017-01-30 09:52:35 +01:00
Jean-Christophe Filliatre
013e16e103 python: better syntax trees (flattened) 2017-01-30 09:08:52 +01:00
Jean-Christophe Filliatre
c51e9e1135 python: more term syntax 2017-01-30 07:57:19 +01:00
Jean-Christophe Filliatre
70a1f7dfd8 python: logical annotations 2017-01-29 16:57:49 +01:00
Jean-Christophe Filliatre
85fa13a141 python: translation to Why3 abstract syntax 2017-01-29 15:52:12 +01:00
Jean-Christophe Filliatre
aa52f5a827 A new plugin to read Python programs
for teaching purposes only
limited to a microscopic fragment of Python for the moment
2017-01-29 13:02:04 +01:00