|
# 1 "/fast/klever/klever-work/native-scheduler/scheduler/jobs/ee95807b-3ddf-440d-8f53-06175ccf37ce/klever-core-work-dir/job/vtg/wget/empty/weaver/aspect"
|
|
# 1 "<built-in>"
|
|
# 1 "<command-line>"
|
|
# 1 "/fast/klever/klever-work/native-scheduler/scheduler/jobs/ee95807b-3ddf-440d-8f53-06175ccf37ce/klever-core-work-dir/job/vtg/wget/empty/weaver/aspect"
|
|
/*
|
|
* Copyright (c) 2018 ISP RAS (http://www.ispras.ru)
|
|
* Ivannikov Institute for System Programming of the Russian Academy of Sciences
|
|
*
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
* you may not use this file except in compliance with the License.
|
|
* You may obtain a copy of the License at
|
|
*
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
* See the License for the specific language governing permissions and
|
|
* limitations under the License.
|
|
*/
|
|
|
|
before: file ("$this")
|
|
{
|
|
int ldv_fork(void);
|
|
}
|
|
|
|
around: call($ fork(..)) ||
|
|
call($ vfork(..))
|
|
{
|
|
return ldv_fork();
|
|
}
|
|
|
|
|
|
|
|
/*
|
|
* Copyright (c) 2018 ISP RAS (http://www.ispras.ru)
|
|
* Ivannikov Institute for System Programming of the Russian Academy of Sciences
|
|
*
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
* you may not use this file except in compliance with the License.
|
|
* You may obtain a copy of the License at
|
|
*
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
* See the License for the specific language governing permissions and
|
|
* limitations under the License.
|
|
*/
|
|
|
|
before: file("$this")
|
|
{
|
|
#include <verifier/memory.h>
|
|
struct globals;
|
|
static struct globals *ldv_globals;
|
|
void ldv_setup_common_bufsiz(void);
|
|
}
|
|
|
|
around: define(setup_common_bufsiz())
|
|
{
|
|
ldv_setup_common_bufsiz()
|
|
}
|
|
|
|
around: define(G)
|
|
{
|
|
(*ldv_globals)
|
|
}
|
|
|
|
after: file("$this")
|
|
{
|
|
#ifdef G
|
|
void ldv_setup_common_bufsiz(void) {
|
|
ldv_globals = ldv_xzalloc(sizeof(struct globals));
|
|
}
|
|
#endif
|
|
}/*
|
|
* Copyright (c) 2018 ISP RAS (http://www.ispras.ru)
|
|
* Ivannikov Institute for System Programming of the Russian Academy of Sciences
|
|
*
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
* you may not use this file except in compliance with the License.
|
|
* You may obtain a copy of the License at
|
|
*
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
* See the License for the specific language governing permissions and
|
|
* limitations under the License.
|
|
*/
|
|
|
|
|
|
before: file("$this")
|
|
{
|
|
extern void ldv_bb_show_usage(void);
|
|
}
|
|
|
|
around: call(void bb_show_usage(..))
|
|
{
|
|
ldv_bb_show_usage();
|
|
}
|
|
|
|
/*
|
|
* Copyright (c) 2018 ISP RAS (http://www.ispras.ru)
|
|
* Ivannikov Institute for System Programming of the Russian Academy of Sciences
|
|
*
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
* you may not use this file except in compliance with the License.
|
|
* You may obtain a copy of the License at
|
|
*
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
* See the License for the specific language governing permissions and
|
|
* limitations under the License.
|
|
*/
|
|
|
|
|
|
before: file("$this")
|
|
{
|
|
extern void ldv_bb_simple_perror_msg_and_die(void);
|
|
}
|
|
|
|
around: call(void bb_error_msg_and_die(..))
|
|
{
|
|
ldv_bb_simple_perror_msg_and_die();
|
|
|
|
}
|
|
|
|
around: call(void bb_perror_msg_and_die(..))
|
|
{
|
|
ldv_bb_simple_perror_msg_and_die();
|
|
|
|
}
|
|
|
|
around: call(void bb_simple_perror_msg(..))
|
|
{
|
|
ldv_bb_simple_perror_msg_and_die();
|
|
|
|
}
|
|
|
|
around: call(void bb_simple_perror_msg_and_die(..))
|
|
{
|
|
ldv_bb_simple_perror_msg_and_die();
|
|
|
|
}
|
|
/*
|
|
* Copyright (c) 2018 ISP RAS (http://www.ispras.ru)
|
|
* Ivannikov Institute for System Programming of the Russian Academy of Sciences
|
|
*
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
* you may not use this file except in compliance with the License.
|
|
* You may obtain a copy of the License at
|
|
*
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
* See the License for the specific language governing permissions and
|
|
* limitations under the License.
|
|
*/
|
|
|
|
|
|
before: file("$this")
|
|
{
|
|
extern void ldv_bb_error_msg_and_die(void);
|
|
}
|
|
|
|
around: call(void bb_error_msg_and_die(..))
|
|
{
|
|
ldv_bb_error_msg_and_die();
|
|
}
|
|
/*
|
|
* Copyright (c) 2018 ISP RAS (http://www.ispras.ru)
|
|
* Ivannikov Institute for System Programming of the Russian Academy of Sciences
|
|
*
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
* you may not use this file except in compliance with the License.
|
|
* You may obtain a copy of the License at
|
|
*
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
* See the License for the specific language governing permissions and
|
|
* limitations under the License.
|
|
*/
|
|
|
|
before: file("$this")
|
|
{
|
|
extern char* ldv_xasprintf(void);
|
|
}
|
|
|
|
around: call(char* xasprintf(..))
|
|
{
|
|
return ldv_xasprintf();
|
|
}/*
|
|
* Copyright (c) 2018 ISP RAS (http://www.ispras.ru)
|
|
* Ivannikov Institute for System Programming of the Russian Academy of Sciences
|
|
*
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
* you may not use this file except in compliance with the License.
|
|
* You may obtain a copy of the License at
|
|
*
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
* See the License for the specific language governing permissions and
|
|
* limitations under the License.
|
|
*/
|
|
|
|
/*
|
|
TODO: Fis CIF to make this code below work
|
|
before: file("$this")
|
|
{
|
|
extern int ldv_asprintf(char **ptr);
|
|
}
|
|
|
|
around: call(int vasprintf(..))
|
|
{
|
|
return ldv_asprintf($arg1);
|
|
}
|
|
*//*
|
|
* Copyright (c) 2018 ISP RAS (http://www.ispras.ru)
|
|
* Ivannikov Institute for System Programming of the Russian Academy of Sciences
|
|
*
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
* you may not use this file except in compliance with the License.
|
|
* You may obtain a copy of the License at
|
|
*
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
* See the License for the specific language governing permissions and
|
|
* limitations under the License.
|
|
*/
|
|
|
|
before: file("$this")
|
|
{
|
|
extern void ldv_exit(void);
|
|
}
|
|
|
|
around: call(void exit(..))
|
|
{
|
|
ldv_exit();
|
|
}
|
|
/*
|
|
* Copyright (c) 2018 ISP RAS (http://www.ispras.ru)
|
|
* Ivannikov Institute for System Programming of the Russian Academy of Sciences
|
|
*
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
* you may not use this file except in compliance with the License.
|
|
* You may obtain a copy of the License at
|
|
*
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
* See the License for the specific language governing permissions and
|
|
* limitations under the License.
|
|
*/
|
|
|
|
before: file("$this")
|
|
{
|
|
#include <stddef.h>
|
|
extern char *ldv_strdup(const char *s);
|
|
extern char *ldv_strcpy(char *dest, const char *src);
|
|
extern char *ldv_strncpy(char *dest, const char *src, size_t n);
|
|
extern size_t ldv_strlen(const char *s);
|
|
}
|
|
|
|
around: call(char *strdup(..))
|
|
{
|
|
return ldv_strdup($arg1);
|
|
}
|
|
|
|
around: call(char *strcpy(..))
|
|
{
|
|
return ldv_strcpy($arg1, $arg2);
|
|
}
|
|
|
|
around: call(char *strncpy(..))
|
|
{
|
|
return ldv_strncpy($arg1, $arg2, $arg3);
|
|
}
|
|
|
|
around: call(size_t strlen(..))
|
|
{
|
|
return ldv_strlen($arg1);
|
|
}
|
|
before: file ("$this")
|
|
{
|
|
#include <verifier/common.h>
|
|
#include <verifier/nondet.h>
|
|
#include <verifier/memory.h>
|
|
#include <userspace/ldv.h>
|
|
|
|
}
|
|
|
|
after: file ("$this")
|
|
{
|
|
}
|