How to deal error "fatal error C1034: stdio.h: no include path set"

[Dinh Ngoc Thi]

Hi

When I use satabs to verify my program which was created by MS Visual studio,
I always meet error message "fatal error C1034: stdio.h: no include path set" although this file  stdio.h is existed in my PC.

So anyone can help me to solve this problem?
Many thanks in advance.

[Michael Tautschnig]

Hello,

Can you confirm that you are running satabs from within the Visual Studio
Command prompt?

Best,
Michael

[Dinh Ngoc Thi]

Thank you Michael.

I solved my problem by using the Visual Studio Command prompt.

[Dinh Ngoc Thi]

Dear Micheal

Although I used Visual Studio Command prompt to run CBMC, but when I use command [cbmc Access_to_ViewView.cpp --function WhatAmI],
I always receive error message as below:
--------
file Access_to_ViewView.cpp: Parsing
Access_to_ViewView.cpp
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlcore.h line 630: parse error before `auto pfSetDefaultDllDirectories = reinterpret_cast'
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlcore.h line 630: parse error before `else { pfSetDefaultDllDirectories ='
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlcore.h line 630: parse error before `} if ( pfSetDefaultDllDirectories'
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlcore.h line 633: parse error before `} WCHAR wszLoadPath ['
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlcore.h line 639: parse error before `if ( rc =='
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlcore.h line 642: parse error before `} if ( wszLoadPath'
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlcore.h line 649: parse error before `} } if ('
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlcore.h line 655: parse error before `} return ( ::'
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlcore.h line 659: parse error before `} } namespace ATL'
file C:\Program Files\Microsoft Visual Studio 12.0\VC\ATLMFC\INCLUDE\atlmem.h line 30: parse error before `} template < typename'
PARSING ERROR
--------

I downloaded file Access_to_ViewView.cpp from CodeProject as attachment.

Could you please give me some recommendation?

[Martin Brain]

The errors are being generated by the code in atlmem.h. Without a copy
of this it is difficult to speculate what is causing the error. It may
be that it is using C++11 features that are not yet supported in CBMC.

Cheers,
- Martin

[Dinh Ngoc Thi]

Dear Martin,

Do you mean there are 11 features of C++ that are not yet supported in CBMC?

Could you please teach me about them?

Also if I compile successfully my C or C++ programs by using Microsoft Visual Studio, so can I verify them  by cbmc?

[Martin Brain]

On Wed, 2014-06-25 at 07:52 -0700, Dinh Ngoc Thi wrote:
> Dear Martin,
>
> Do you mean there are 11 features of C++ that are not yet supported in CBMC?

Not quite; what I mean is that there are some features that were added
to the C++ language in ISO/IEC 14882:2011 (informally known as "C++11")
that are not supported by CBMC at the moment. For more information on
the different versions of C++, see:

http://en.wikipedia.org/wiki/C++#Standardization

> Could you please teach me about them?
>
>
> Also if I compile successfully my C or C++ programs by using Microsoft
> Visual Studio, so can I verify them by cbmc?

Maybe. CBMC has (I believe) complete support for C99, support for the
commonly used parts of C11 and a variety of compiler specific
extensions, including some from GCC. Microsoft Visual Studio does not
fully support C99 and has some extensions. Thus there are some valid
C99 programs that you can verify with CBMC but not compile with Visual
Studio and some programs in Microsoft's extension of C that you can
compile with Visual Studio but will not parse in CBMC. If you stick to
C99 (gcc has the flag -std=c99 which can check this) then it is likely
that you can compile things in Visual Studio and verify them using CBMC.

The picture for C++ is a little more complicated. C++ is a very large
and complex language with a lot of obscure and little used features.
Writing a complete C++ front-end is a very time consuming process (note
that most compilers do not implement the full language). Thus the C++
front-end for CBMC includes the parts of C++ that are commonly used in
embedded applications plus a number of other features that particular
customers have needed for their project. We support much of the core of
C++98 and C++03 although our support for template meta-programming could
be improved. We don't support many of the new features added in C++11
as some of them are a lot of work and we have yet to find a pressing
need for them. Thus for C++ there will be more programs that compile in
Visual Studio (some of which will not be standards compliant C++) that
will not parse in CBMC.

If you are starting a new project from scratch and want to use CBMC I
would suggest using C99. If you have a program that does not parse and
you would like it to, please send us a minimal test case and we'll add
it to the todo list. If you need more prompt support for a particular
feature, contact us directly and we can probably work something out.

Does that help?

Cheers,
- Martin

[Dinh Ngoc Thi]

Dear Martin

I greatly appreciate your details of reply.
Now I understood the between of parsing between CBMC and Microsoft Visual Studio.

[Thuan Doan]

hello, I'm trying to run a C program using command prompt, but failed with the same problem of you. that is "fatal error C1034: stdio.h: no include path set". I try to google, but have no proper answer. can u show me your solution

[Michael Tautschnig]

Hello,

> hello, I'm trying to run a C program using command prompt, but failed with
> the same problem of you. that is "fatal error C1034: stdio.h: no include
> path set". I try to google, but have no proper answer. can u show me your
> solution
>

[...]

Can you please confirm that you are running CBMC (or whichever CProver tool you
might be running) from the "Visual Studio Command Prompt"? In this very setting,
you should also confirm that you can compile the program (using cl).

Best,
Michael