21 Commits

Author	SHA1	Message	Date
Kyriakos Georgiou	aa450e7ce9	adding the makefile for the cortexM7 board	2020-11-16 13:49:57 +00:00
Kyriakos Georgiou	aec89f2a9c	changing version of the Ada Arm compiler used	2020-11-10 21:08:00 +00:00
Kyriakos Georgiou	5dd8631bdb	fixig bug in Makefile to use Cortex-m4 and 2020-arm-elf	2020-11-06 12:25:23 +00:00
Guillaume	f59cb239b3	Add a support for the stm32f407 platform. ... configure.sh is a script to determine which target must be used for the compilation.	2020-11-05 16:23:39 +01:00
Guillaume Cluzel	0f95b022ce	Add a preprocessing option to enable or disable support for UDP	2020-08-28 14:39:26 +02:00
Guillaume Cluzel	ea17ad063e	Add support for all the preprocessed constants of the C code in the SPARK code	2020-08-28 14:39:26 +02:00
Guillaume Cluzel	7e7333f0cd	Test for preprocessing	2020-08-28 14:39:25 +02:00
Guillaume Cluzel	7abad46431	Update README	2020-08-03 11:16:40 +02:00
Guillaume Cluzel	4288db5291	Update README	2020-08-03 09:33:40 +02:00
Guillaume Cluzel	5e66197a15	Corrections in the Makefile	2020-07-31 14:32:24 +02:00
Guillaume Cluzel	a5a2c4ab53	Improvement in code and proofs	2020-07-19 19:06:02 +02:00
Guillaume Cluzel	7ce62a46b0	Some corrections in the contracts	2020-07-09 09:43:29 +02:00
Guillaume Cluzel	a1f497c154	Add functions to simplify use in loop invariants	2020-07-06 14:06:17 +02:00
Guillaume Cluzel	039982c2d1	update compilation options	2020-07-03 10:45:38 +02:00
Guillaume Cluzel	b8b819449f	Improve Ada Style	2020-07-01 15:55:42 +02:00
Guillaume Cluzel	25a67a3373	Add Tcp_Abort	2020-05-07 10:28:28 +02:00
Guillaume Cluzel	4bb3cd8852	reimplementation of sockets	2020-04-29 22:54:36 +02:00
Guillaume Cluzel	8e01250f34	prove target	2020-04-08 14:06:18 +02:00
Guillaume Cluzel	ade629ecdc	Ada binding	2020-04-03 16:07:30 +02:00
Guillaume Cluzel	b75627b9cb	socketOpen binding	2020-03-30 23:29:03 +02:00
Guillaume Cluzel	bf848defd5	Initial commit	2020-03-25 14:21:41 +01:00