Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
No subject
- Subject: No subject
- From: bogus@does.not.exist.com ()
- Date: Fri, 19 Dec 2008 07:15:14 -0000
forward slashes and backward slashes. (2) Also, on a slightly related problem, I experienced an odd problem on my home laptop. I downloaded and installed Z3 without any problems, i.e., I am able to invoke it from a DOS command shell). However, when I ran the why-config utility, there was a problem with respect to the detection of the Z3 prover. Has anyone else encountered this? I was able to confirm that there was a problem when I tried to invoke Z3 directly from within a Cygwin shell. The output from the why-config call is below: $ why-config starting autodetection... 'alt-ergo' is not recognized as an internal or external command, operable program or batch file. command alt-ergo failed Found prover Alt-Ergo version 0.8 Found prover Simplify version 1.5.4 The system cannot execute the specified program. command z3 failed The system cannot execute the specified program. command z3 failed detection of prover Z3 failed Found prover Yices version 1.0.15 Found prover CVC3 version 1.5 Found prover Coq version 8.1pl4 detection done. writing rc file... Any thoughts on what can be done to resolve these problems? Thanks, Juan ------=_NextPart_000_0000_01C96444.67C99E30 Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable <html xmlns:o=3D"urn:schemas-microsoft-com:office:office" = xmlns:w=3D"urn:schemas-microsoft-com:office:word" = xmlns:st1=3D"urn:schemas-microsoft-com:office:smarttags" = xmlns=3D"http://www.w3.org/TR/REC-html40";> <head> <META HTTP-EQUIV=3D"Content-Type" CONTENT=3D"text/html; = charset=3Dus-ascii"> <meta name=3DGenerator content=3D"Microsoft Word 11 (filtered medium)"> <o:SmartTagType = namespaceuri=3D"urn:schemas-microsoft-com:office:smarttags" name=3D"place"/> <!--[if !mso]> <style> st1\:*{behavior:url(#default#ieooui) } </style> <![endif]--> <style> <!-- /* Style Definitions */ p.MsoNormal, li.MsoNormal, div.MsoNormal {margin:0cm; margin-bottom:.0001pt; font-size:12.0pt; font-family:"Times New Roman";} a:link, span.MsoHyperlink {color:blue; text-decoration:underline;} a:visited, span.MsoHyperlinkFollowed {color:purple; text-decoration:underline;} span.EmailStyle17 {mso-style-type:personal-compose; font-family:Arial; color:windowtext;} @page Section1 {size:612.0pt 792.0pt; margin:72.0pt 90.0pt 72.0pt 90.0pt;} div.Section1 {page:Section1;} --> </style> </head> <body lang=3DEN-US link=3Dblue vlink=3Dpurple> <div class=3DSection1> <p class=3DMsoNormal><font size=3D2 face=3DArial><span lang=3DDE = style=3D'font-size:10.0pt; font-family:Arial'>Greetings,<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span lang=3DDE = style=3D'font-size:10.0pt; font-family:Arial'><o:p> </o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'>(1) Here are the results from the call to the Jessie = plugin via setting the FRAMAC_SHARE environment = variable.<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'><o:p> </o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span lang=3DDE style=3D'font-size:10.0pt;font-family:"Courier New"'>$ FRAMAC_SHARE=3D/usr/local/Frama-C/bin/frama-c frama-c -jessie-analysis = -jessie-gui a.c<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt; font-family:"Courier New"'>Parsing<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt; font-family:"Courier New"'>[preprocessing] running gcc -C -E -<st1:place = w:st=3D"on">I.</st1:place> -include <b><font color=3Dnavy><span = style=3D'color:navy;font-weight:bold'>/usr/local/Frama-C/bin/frama-c\jess= ie\jessie_prolog.h</span></font></b> -dD a.c<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt; font-family:"Courier New"'>cc1: <b><font color=3Dnavy><span = style=3D'color:navy; font-weight:bold'>/usr/local/Frama-C/bin/frama-c\jessie\jessie_prolog.h</= span></font></b>: No such file or directory<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt; font-family:"Courier New"'>Failed to run: gcc -C -E -<st1:place = w:st=3D"on">I.</st1:place> -include /usr/local/Frama-C/bin/frama-c\jessie\jessie_prolog.h -dD -o "C:\Users\jua\AppData\Local\Temp\a.c3bc755.i" = "a.c"<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt; font-family:"Courier New"'><o:p> </o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt; font-family:"Courier = New"'> You = may set the CPP environment variable to select the proper preprocessor command = ...<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt; font-family:"Courier New"'> or = use the -cpp-command program argument.<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt; font-family:"Courier New"'>Fatal error: exception Sys_error("C:\Users\sotjua\AppData\Local\Temp\a.c3bc755.i: No such = file or directory")<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'><o:p> </o:p></span></font></p> <p class=3DMsoNormal><b><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial;font-weight:bold'>From the looks of things there = appears to be a problem with respect to forward slashes and backward = slashes.<o:p></o:p></span></font></b></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'><o:p> </o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'>(2) Also, on a slightly related problem, I = experienced an odd problem on my home laptop. I downloaded and installed Z3 without any problems, i.e., I am able to invoke it from a DOS command shell). = <o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'>However, when I ran the <b><span = style=3D'font-weight:bold'>why-config</span></b> utility, there was a problem with respect to the detection of the Z3 = prover. Has anyone else encountered this? I was able to confirm that there was a problem when <o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'>I tried to invoke Z3 directly from within a Cygwin = shell.<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'><o:p> </o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'>The output from the why-config call is = below:<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'><o:p> </o:p></span></font></p> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 = face=3D"Courier New"><span style=3D'font-size:10.0pt;font-family:"Courier New"'>$ = why-config<o:p></o:p></span></font></p> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 = face=3D"Courier New"><span style=3D'font-size:10.0pt;font-family:"Courier New"'>starting = autodetection...<o:p></o:p></span></font></p> <p class=3DMsoNormal style=3D'text-autospace:none'><b><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt;font-family:"Courier New"; font-weight:bold'>'alt-ergo' is not recognized as an internal or = external command, operable program or batch = file.<o:p></o:p></span></font></b></p> <p class=3DMsoNormal style=3D'text-autospace:none'><b><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt;font-family:"Courier New"; font-weight:bold'>command alt-ergo = failed<o:p></o:p></span></font></b></p> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 = face=3D"Courier New"><span style=3D'font-size:10.0pt;font-family:"Courier New"'>Found prover = Alt-Ergo version 0.8<o:p></o:p></span></font></p> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 = face=3D"Courier New"><span style=3D'font-size:10.0pt;font-family:"Courier New"'>Found prover = Simplify version 1.5.4<o:p></o:p></span></font></p> <p class=3DMsoNormal style=3D'text-autospace:none'><b><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt;font-family:"Courier New"; font-weight:bold'>The system cannot execute the specified = program.<o:p></o:p></span></font></b></p> <p class=3DMsoNormal style=3D'text-autospace:none'><b><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt;font-family:"Courier New"; font-weight:bold'>command z3 failed<o:p></o:p></span></font></b></p> <p class=3DMsoNormal style=3D'text-autospace:none'><b><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt;font-family:"Courier New"; font-weight:bold'>The system cannot execute the specified = program.<o:p></o:p></span></font></b></p> <p class=3DMsoNormal style=3D'text-autospace:none'><b><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt;font-family:"Courier New"; font-weight:bold'>command z3 failed<o:p></o:p></span></font></b></p> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 = face=3D"Courier New"><span style=3D'font-size:10.0pt;font-family:"Courier New"'>detection of prover = Z3 failed<o:p></o:p></span></font></p> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 = face=3D"Courier New"><span style=3D'font-size:10.0pt;font-family:"Courier New"'>Found prover Yices = version 1.0.15<o:p></o:p></span></font></p> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 = face=3D"Courier New"><span style=3D'font-size:10.0pt;font-family:"Courier New"'>Found prover CVC3 = version 1.5<o:p></o:p></span></font></p> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 = face=3D"Courier New"><span style=3D'font-size:10.0pt;font-family:"Courier New"'>Found prover Coq = version 8.1pl4<o:p></o:p></span></font></p> <p class=3DMsoNormal style=3D'text-autospace:none'><font size=3D2 = face=3D"Courier New"><span style=3D'font-size:10.0pt;font-family:"Courier New"'>detection = done.<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3D"Courier New"><span = style=3D'font-size:10.0pt; font-family:"Courier New"'>writing rc file...</span></font><font = size=3D2 face=3DArial><span = style=3D'font-size:10.0pt;font-family:Arial'><o:p></o:p></span></font></p= > <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'><o:p> </o:p></span></font></p> <p class=3DMsoNormal><b><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial;font-weight:bold'>Any thoughts on what can be done to = resolve these problems?<o:p></o:p></span></font></b></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'><o:p> </o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'>Thanks,<o:p></o:p></span></font></p> <p class=3DMsoNormal><font size=3D2 face=3DArial><span = style=3D'font-size:10.0pt; font-family:Arial'>Juan</span></font> <font size=3D2 face=3DArial><span style=3D'font-size:10.0pt;font-family:Arial'><o:p></o:p></span></font></p= > <p class=3DMsoNormal><font size=3D3 face=3D"Times New Roman"><span = style=3D'font-size: 12.0pt'><o:p> </o:p></span></font></p> </div> </body> </html> ------=_NextPart_000_0000_01C96444.67C99E30--
- Prev by Date: [Frama-c-discuss] FW: Windows Frama-C Release
- Next by Date: [Frama-c-discuss] Installation Problem
- Previous by thread: No subject
- Next by thread: [Frama-c-discuss] interfacing non-OCaml programs with Frama-C
- Index(es):