7 Commits

Author SHA1 Message Date
naddy
3e042ba62d Bump all ports that depend on ports-gcc on the clang archs.
SYSTEM_VERSION didn't quite work out how we expected and it's
easier|safer to do it this way than fiddle with pkg_add now.
2019-04-28 21:08:26 +00:00
daniel
aa4bbca17d Drop dependency on base gcc and switch to ports gcc instead. 2019-04-20 22:12:41 +00:00
bcallah
155ab44de2 Update to compcert-3.5
ok daniel@ (MAINTAINER)
2019-03-17 03:26:53 +00:00
jca
3e9567b10a Remove BROKEN, math/coq has been updated
ok daniel@ (maintainer)
2019-03-16 18:33:15 +00:00
daniel
98274b8b3f Update to Compcert 3.4. Still marked BROKEN until coq is updated. 2018-10-27 01:16:42 +00:00
daniel
01c5ef0515 Update to CompCert 3.3 as requested by danj@ but mark BROKEN until we
get coq updated. Biggest improvement in this update is support for
amd64.

CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
2018-09-12 04:58:49 +00:00
daniel
3c4bfcc3d7 import lang/compcert. ok sthen@
The CompCert C verified compiler is a compiler for a large subset
of the C programming language that generates code for the PowerPC,
ARM and x86 processors.

The distinguishing feature of CompCert is that it has been formally
verified using the Coq proof assistant: the generated assembly code
is formally guaranteed to behave as prescribed by the semantics of
the source C code.

CompCert is not free software. This non-commercial release can only
be used for evaluation, research, educational and personal purposes.
2015-09-05 00:20:08 +00:00