feat:initial attempts to test tipc;please provide gental feedback#11
feat:initial attempts to test tipc;please provide gental feedback#11YuyanBao wants to merge 2 commits intoseahorn:masterfrom
Conversation
agurfinkel
left a comment
agurfinkel
left a comment
There was a problem hiding this comment.
LGTM
A few minor comments. Most important remove Temporary files that are added by accident.
This is a good start.
| include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/keymaster/include) | ||
| include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/rng/include) | ||
| include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/storage/include) | ||
| include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/tipc/include) |
There was a problem hiding this comment.
it is better to move include directories where they are actually used.
But I guess we can refactor it all at once since other directories are already globally included.
|
|
||
|
|
||
| ssize_t send_msg(handle_t handle, struct ipc_msg *msg); | ||
| int msg_send_called; No newline at end of file |
There was a problem hiding this comment.
comment on what this global variable is for.
By convention, we name globals using g_ prefix, so it should be g_msg_send_called
There was a problem hiding this comment.
Not sure this variable should be declared in the header file.
| @@ -0,0 +1 @@ | |||
| --- | |||
There was a problem hiding this comment.
this file should not have been included.
Same applies to all files in Testing/ directory
| @@ -0,0 +1,3 @@ | |||
| Start testing: May 31 09:46 EDT | |||
There was a problem hiding this comment.
file should not be included
| int main(void) { | ||
| int rc; | ||
| handle_t h = INVALID_IPC_HANDLE; | ||
| char path[64]; |
There was a problem hiding this comment.
This is the example Xiang set for me. The goal is to teach me how to write tests :)
| // msg_is_send_called = 0; | ||
|
|
||
| /* assumptions */ | ||
| msg_send_called = 0; |
There was a problem hiding this comment.
I now understand why the variable is declared in the header file.
Would be cleaner to expose a method to reset the state.
|
|
||
| size_t buf_len = nd_size_t(); | ||
| //void *buf = can_fail_malloc(buf_len); | ||
| void *buf = malloc(buf_len); |
There was a problem hiding this comment.
need to use our allocation library. This has potentially undefined behaviour. The buffer is allocated but is never written to. It is then given to a function that might read from it.
There was a problem hiding this comment.
one way to fix this locally is to call memhavoc after malloc. @danblitzhou can help with that.
|
|
||
| extern handle_t nd_handle(void); | ||
| extern int nd_size_t(void); | ||
| extern void *sea_malloc_havoc(size_t sz); |
There was a problem hiding this comment.
I don't think this function signature is recognized by seahorn op sem; you would still need to implement the actual function sea_malloc_havoc, or copy the existing one from aws c common project
There was a problem hiding this comment.
I guess I have not ported these. They have to be part of our libc port
| #include <trusty_ipc.h> | ||
| #include <sea_tipc_helper.h> | ||
|
|
||
| extern handle_t nd_handle(void); |
There was a problem hiding this comment.
include nondet.h and use functions from there instead
3 participants
It is just a very simple test for me to figure out the structure and the way to add tests. Please tell me if it is the correct way to do it.