Benjamin Nauck hyarion

hyarion / [WIP] ACSL by Example Report

Created December 17, 2018 00:17

	# this is the current state of running the test suite from "ACSL by Example"
	# a few goals fails here and there.. I need to figure out how to check exactly
	# which one it is

	# bumped the env waay up to make sure those wheren't the cause
	$ echo $WP_TIMEOUT $WP_COQ_TIMEOUT $WP_ALT_ERGO_STEPS
	80 80 20000

	$ why3 --version
	Why3 platform, version 1.1.0

hyarion / frama-c+why3.1.1.0.log

Created December 11, 2018 23:34

[WIP] Frama-C 18.0 (Argon) + Why3 1.1.0

	hyarion$ frama-c -wp -wp-prover=cvc4,z3-ce isqrt.c
	[kernel] Parsing isqrt.c (with preprocessing)
	[wp] Warning: Missing RTE guards
	[wp] 61 goals scheduled
	[wp] Proved goals: 61 / 61
	Qed: 41 (0.30ms-14ms-56ms)
	cvc4: 2 (140ms)
	z3-ce: 19 (30ms-221ms-1.8s)
	hyarion$ why3 --version
	Why3 platform, version 1.1.0

hyarion / toolchain-nacl.cmake

Created March 1, 2012 09:26

native client cmake toolchain file (from /seichter/CMake-Toolchain-Collection)

	#
	# Google Native Client toolchain file for CMake
	#
	# (c) Copyrights 2009-2011 Hartmut Seichter
	#
	# Note: only works on OSX
	#

	set(NACL_PATH $ENV{NACL_ROOT} CACHE STRING "Native Client SDK Root Path")