Skip to content

goto-instrument: handling of VarArgs #934

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
stahlbauer opened this issue May 17, 2017 · 4 comments
Closed

goto-instrument: handling of VarArgs #934

stahlbauer opened this issue May 17, 2017 · 4 comments

Comments

@stahlbauer
Copy link
Contributor

stahlbauer commented May 17, 2017

It would be great if goto-instrument would be able to handle variable arguments and dump valid C code; example of a program that is not yet fully covered by the implementation:

#include<stdarg.h>
#include<stdlib.h>

void bb_verror_msg(const char *s, va_list p, const char *strerr) {
}

void bb_error_msg(const char *s, ...)
{
    va_list p;
    va_start(p, s);
    bb_verror_msg(s, p, NULL);
    va_end(p);
}

int main() {
    bb_error_msg("FOOO");
    return 0;
}

GCC complains about when parsing the file that was produced by goto-instrument:

error: cast specifies array type
   va_list p=(va_list)&s;
             ^
error: cast specifies array type
   p = ((va_list)NULL);

clang states that:

error: used type 'va_list' (aka
      '__builtin_va_list') where arithmetic or pointer type is
      required
  va_list p=(va_list)&s;
            ^        ~~
error: used type 'va_list' (aka
      '__builtin_va_list') where arithmetic or pointer type is
      required
  p = ((va_list)((void*)0));
@stahlbauer
Copy link
Contributor Author

@tautschnig FYI

@stahlbauer
Copy link
Contributor Author

stahlbauer commented May 17, 2017

A workaround would be a feature that abstracts away (declare them as extern) the definitions of some functions. For example, functions with variable argument list.

@stahlbauer
Copy link
Contributor Author

The hackiest and ugliest solution I can imagine would be something like:

os_body << "// " << symbol.name << std::endl;
os_body << "// " << symbol.location << std::endl;
const std::string &fn_decl_str = make_decl(symbol.name, symbol.type);
if (fn_decl_str.find("...")==std::string::npos
    && fn_decl_str.find("va_list")==std::string::npos) {
  os_body<<fn_decl_str<<std::endl;
  os_body<<expr_to_string(b);
  os_body<<std::endl<<std::endl;
} else {
  if (fn_decl_str.find("extern ")==std::string::npos) {
    os_body<<"extern ";
  }
  os_body<<fn_decl_str<<";";
  os_body<<std::endl;
}

@stahlbauer
Copy link
Contributor Author

The problem is still there. Functions with va_list parameters cause problems. For example, if the "va_list" gets assigned to a void** pointer.

@stahlbauer stahlbauer changed the title Goto-Instrument: Handling of VarArgs goto-instrument: handling of VarArgs May 26, 2017
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jun 8, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant