/src/backends/Horn - Repository - LustreC

| Branch: | Tag: | Revision:

lustrec/src/backends/Horn @ c85c2e3d

Name	Size	Revision	Age	Author	Comment
.merlin	3 Bytes	ae7d913d	almost 5 years	Pierre-Loïc Garoche	Merlin files
horn_backend.ml	4.26 KB	83dc064f	about 5 years	Pierre-Loïc Garoche	Byte/String bug reappeared
horn_backend_collecting_sem.ml	7.66 KB	089f94be	over 5 years	Pierre-Loïc Garoche	MLI for normalization and machine_code. Structs...
horn_backend_common.ml	5.29 KB	2863281f	over 5 years	Pierre-Loïc Garoche	Further restructuring: - arrow.ml* to define ba...
horn_backend_printers.ml	26.6 KB	c35de73b	almost 5 years	Pierre-Loïc Garoche	Pretty serious update: - a bug in regressio nte...
horn_backend_traces.ml	8.51 KB	0d54d8a8	almost 5 years	Pierre-Loïc Garoche	Removed Contract contruct: imported node should...

#	Date	Author	Comment
ae7d913d	11/16/2018 04:18 AM	Pierre-Loïc Garoche	Merlin files
c35de73b	11/15/2018 03:18 AM	Pierre-Loïc Garoche	Pretty serious update: - a bug in regressio ntest Simulink/integrator_ext_IC_matrix_test revealed the following (serious issue): when building the list of instruction (in the machine code) the access to variable were hardcoded to LocalVar or StateVAr depending whether the variables was part of the identified memories....
0d54d8a8	11/13/2018 02:01 AM	Pierre-Loïc Garoche	Removed Contract contruct: imported node should be enough. Solved some warning at compile time
83dc064f	07/13/2018 08:05 PM	Pierre-Loïc Garoche	Byte/String bug reappeared
f9d0c175	07/13/2018 07:52 PM	Pierre-Loïc Garoche	Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec
2d2144c0	07/13/2018 05:18 PM	Pierre-Loïc Garoche	Solved bug#57: issues when indirect init of a pre in horn-traces
bec3cf3d	05/31/2018 04:35 PM	Xavier Thirioux	strange bug (ill-typed source) wrt Bytes/String conversion
1d0fd52b	05/18/2018 12:28 AM	Xavier Thirioux	updated division for Horn clauses
fa91d4d0	05/17/2018 03:14 PM	Pierre-Loïc Garoche	Euclidean div/mod treatment in Horn backend
ea8f51ae	03/30/2018 11:23 PM	Pierre-Loïc Garoche	Basic library printers moved into backend specific printer files

Also available in: Atom