"arraysum", "csv" => "csv", "mergesort" => "mergesort", "stringlist" => "stringlist", "sumreduce" => "sumreduce", ); $demo = "stringlist"; function getRawTextFromField($fld){ return stripslashes($_POST[$fld]); } function writeTextFile($fname,$fld){ $f = fopen($fname, "w"); fwrite($f,getRawTextFromField($fld)); fclose($f); } function getFieldOrFile ($entered_program, $field, $filename) { if($entered_program == 1) { return (htmlspecialchars (getRawTextFromField ($field))); } else { return (htmlspecialchars (file_get_contents ($filename))); } } if($_POST['programform'] == "1") { $tb = tempnam ("/tmp/csolve-demo", "csolve-demo-"); $tc = $tb . ".c"; $tobj = $tb . ".o"; $tann = $tobj . ".annot"; $thq = $tobj . ".hquals"; $thtml = $tobj . ".html"; $log = $tobj . ".log"; writeTextFile($tc, 'program'); writeTextFile($thq, 'qualifiers'); $status = 0; $out = array(); exec("../src/csolve --web-demo -c ".$tc." -o ".$tobj." 2>&1", $out, $status); $annothtml = file_get_contents ($thtml); $entered_program = 1; } if($_POST['chooseform'] == "1" || $entered_program) { $demo = $category[$_POST['demo']]; } ?> CSolve Demo
CSolve Demo
Liquid Types-Based C Program Verifier
Safe
Unsafe

Pick a demo

' method='post'>

Each demo consists of a C program and the predicate templates required to verify its safety.

You may also try your own programs, in which case you may want to refer to the CSolve README.

' method='post' onSubmit='setTextAreaValue ("program", editor); setTextAreaValue ("qualifiers", qualEditor)'>

C Program

Predicate Templates